let G be _Graph; :: thesis: for H being Subgraph of G holds H .allConnectedSG() c= G .allConnectedSG()
let H be Subgraph of G; :: thesis: H .allConnectedSG() c= G .allConnectedSG()

now :: thesis: for x being object st x in H .allConnectedSG() holds
x in G .allConnectedSG()

let x be object ; :: thesis: ( x in H .allConnectedSG() implies x in G .allConnectedSG() )
assume x in H .allConnectedSG() ; :: thesis: x in G .allConnectedSG()
then reconsider H9 = x as connected plain Subgraph of H by Th124;
H9 is Subgraph of G by GLIB_000:43;
hence x in G .allConnectedSG() by Th124; :: thesis: verum

end;

hence H .allConnectedSG() c= G .allConnectedSG() by TARSKI:def 3; :: thesis: verum