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

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

assume G2 in G1 .allConnectedSG() ; :: thesis: G2 is connected plain Subgraph of G1
then consider H being Element of [#] (G1 .allSG()) such that
A1: ( G2 = H & H is connected ) ;
thus G2 is connected plain Subgraph of G1 by A1; :: thesis: verum

end;

assume A2: G2 is connected plain Subgraph of G1 ; :: thesis: G2 in G1 .allConnectedSG()
then G2 in [#] (G1 .allSG()) by Th1;
hence G2 in G1 .allConnectedSG() by A2; :: thesis: verum