let G1, G2 be Graph; ( 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 )
; ( ( not G1 \/ G2 = G2 & not G2 \/ G1 = G2 ) or G1 c= G2 )
assume A2:
( G1 \/ G2 = G2 or G2 \/ G1 = G2 )
; G1 c= G2
A3:
the carrier of G2 = the carrier of G1 \/ the carrier of G2
by A1, A2, Def3;
A4:
the carrier of G1 c= the carrier of G2
by A3, XBOOLE_1:7;
A5:
the carrier' of G2 = the carrier' of G1 \/ the carrier' of G2
by A1, A2, Def3;
A6:
the carrier' of G1 c= the carrier' of G2
by A5, XBOOLE_1:7;
A7:
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 ;
( 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
;
( 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 )
thus A9:
the
Source of
G1 . v = the
Source of
G2 . v
by A1, A2, A8, Def3;
( 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;
( 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;
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;
verum
end;
A11:
G1 is Subgraph of G2
by A4, A6, A7, Def18;
thus
G1 c= G2
by A11, Def24; verum