let G1, G2 be Graph; :: thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & ( G1 \/ G2 = G2 or G2 \/ G1 = G2 ) implies G1 c= G2 )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; :: thesis: ( ( not G1 \/ G2 = G2 & not G2 \/ G1 = G2 ) or G1 c= G2 )
assume A2: ( G1 \/ G2 = G2 or G2 \/ G1 = G2 ) ; :: thesis: G1 c= G2
then the carrier of G2 = the carrier of G1 \/ the carrier of G2 by A1, Def5;
then A3: the carrier of G1 c= the carrier of G2 by XBOOLE_1:7;
the carrier' of G2 = the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5;
then A4: the carrier' of G1 c= the carrier' of G2 by XBOOLE_1:7;
for v being set st v in the carrier' of G1 holds
( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 )
proof
let v be set ; :: thesis: ( v in the carrier' of G1 implies ( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 ) )
assume A5: v in the carrier' of G1 ; :: thesis: ( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 )
hence A6: the Source of G1 . v = the Source of G2 . v by A1, A2, Def5; :: thesis: ( the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 )
thus A7: the Target of G1 . v = the Target of G2 . v by A1, A2, A5, Def5; :: thesis: ( the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 )
thus the Source of G2 . v in the carrier of G1 by A5, A6, FUNCT_2:5; :: thesis: the Target of G2 . v in the carrier of G1
thus the Target of G2 . v in the carrier of G1 by A5, A7, FUNCT_2:5; :: thesis: verum
end;
then G1 is Subgraph of G2 by A3, A4, Def18;
hence G1 c= G2 ; :: thesis: verum