thus not G .allSG() is empty by Th3; :: thesis: ( G .allSG() is \/-tolerating & G .allSG() is plain )

now :: thesis: for H1, H2 being _Graph st H1 in G .allSG() & H2 in G .allSG() holds
H1 tolerates H2

let H1, H2 be _Graph; :: thesis: ( H1 in G .allSG() & H2 in G .allSG() implies H1 tolerates H2 )
assume ( H1 in G .allSG() & H2 in G .allSG() ) ; :: thesis: H1 tolerates H2
then ( H1 is Subgraph of G & H2 is Subgraph of G ) by Th1;
hence H1 tolerates H2 by GLIB_014:14; :: thesis: verum

end;

hence G .allSG() is \/-tolerating by GLIB_014:def 23; :: thesis: G .allSG() is plain
for H being _Graph st H in G .allSG() holds
H is plain by Th1;
hence G .allSG() is plain by GLIB_014:def 2; :: thesis: verum