FDL > PVS > Graphs > subgraphs > subgraph lem > pf:subgraph lem > 1

Conclusion

1. subgraph?(subgraph(G!1, V!1), G!1)