let G1, G2 be _Graph; :: thesis: ( G2 in G1 .allSG() iff G2 is plain Subgraph of G1 )

hereby :: thesis: ( G2 is plain Subgraph of G1 implies G2 in G1 .allSG() )

assume G2 in G1 .allSG() ; :: thesis: G2 is plain Subgraph of G1
then consider V being non empty Subset of (the_Vertices_of G1), E being Subset of (the_Edges_of G1) such that
A1: G2 = the plain inducedSubgraph of G1,V,E and
E c= G1 .edgesBetween V ;
thus G2 is plain Subgraph of G1 by A1; :: thesis: verum

end;

assume A2: G2 is plain Subgraph of G1 ; :: thesis: G2 in G1 .allSG()
set G9 = the plain inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2;
A3: ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 ) by A2, GLIB_000:def 32;
G2 .edgesBetween (the_Vertices_of G2) c= G1 .edgesBetween (the_Vertices_of G2) by A2, GLIB_000:76;
then A4: the_Edges_of G2 c= G1 .edgesBetween (the_Vertices_of G2) by GLIB_000:34;
( the_Vertices_of the plain inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2 = the_Vertices_of G2 & the_Edges_of the plain inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2 = the_Edges_of G2 ) by A3, A4, GLIB_000:def 37;
then the plain inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2 = G2 by A2, GLIB_000:86, GLIB_009:44;
hence G2 in G1 .allSG() by A3, A4; :: thesis: verum