let G1, G2 be strict Graph; :: thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & bool (G1 \/ G2) c= (bool G1) \/ (bool G2) & not G1 c= G2 implies G2 c= G1 )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; :: thesis: ( not bool (G1 \/ G2) c= (bool G1) \/ (bool G2) or G1 c= G2 or G2 c= G1 )
assume A2: bool (G1 \/ G2) c= (bool G1) \/ (bool G2) ; :: thesis: ( G1 c= G2 or G2 c= G1 )
A3: G1 \/ G2 in bool (G1 \/ G2) by Th29;
A4: now :: thesis: ( G1 \/ G2 in bool G1 implies G2 c= G1 )
assume G1 \/ G2 in bool G1 ; :: thesis: G2 c= G1
then G1 \/ G2 is Subgraph of G1 by Def25;
then A5: G1 \/ G2 c= G1 ;
G1 c= G1 \/ G2 by A1, Th19;
then G1 \/ G2 = G1 by A5, Th16;
hence G2 c= G1 by A1, Th24; :: thesis: verum
end;
now :: thesis: ( G1 \/ G2 in bool G2 implies G1 c= G2 )
assume G1 \/ G2 in bool G2 ; :: thesis: G1 c= G2
then G1 \/ G2 is Subgraph of G2 by Def25;
then A6: G1 \/ G2 c= G2 ;
G2 c= G1 \/ G2 by A1, Th19;
then G1 \/ G2 = G2 by A6, Th16;
hence G1 c= G2 by A1, Th24; :: thesis: verum
end;
hence ( G1 c= G2 or G2 c= G1 ) by A2, A3, A4, XBOOLE_0:def 3; :: thesis: verum