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, Def3;
then A4: 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, Def3;
then A6: 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 A8: 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 A9: the Source of G1 . v = the Source of G2 . v by A1, A2, Def3; :: 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 A10: the Target of G1 . v = the Target of G2 . v by A1, A2, A8, Def3; :: 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 A8, A9, FUNCT_2:7; :: thesis: the Target of G2 . v in the carrier of G1
thus the Target of G2 . v in the carrier of G1 by A8, A10, FUNCT_2:7; :: thesis: verum

end;

then G1 is Subgraph of G2 by A4, A6, Def18;
hence G1 c= G2 by Def24; :: thesis: verum