let G, G1, G2, G3 be Graph; :: thesis: ( G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 implies G c= G3 )
assume that
A1: G1 c= G3 and
A2: G2 c= G3 and
A3: G is_sum_of G1,G2 ; :: thesis: G c= G3
A4: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by A3;
A5: MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 by A3;
A6: G1 is Subgraph of G3 by A1;
A7: G2 is Subgraph of G3 by A2;
A8: the carrier of G1 c= the carrier of G3 by A6, Def18;
the carrier of G2 c= the carrier of G3 by A7, Def18;
then A9: the carrier of G1 \/ the carrier of G2 c= the carrier of G3 by A8, XBOOLE_1:8;
A10: the carrier' of G1 c= the carrier' of G3 by A6, Def18;
the carrier' of G2 c= the carrier' of G3 by A7, Def18;
then A11: the carrier' of G1 \/ the carrier' of G2 c= the carrier' of G3 by A10, XBOOLE_1:8;
for v being set st v in the carrier' of (G1 \/ G2) holds
( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) )

proof

let v be set ; :: thesis: ( v in the carrier' of (G1 \/ G2) implies ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) ) )
assume A12: v in the carrier' of (G1 \/ G2) ; :: thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) )
thus A13: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) :: thesis: ( the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) )

proof

A14: v in the carrier' of G1 \/ the carrier' of G2 by A4, A12, Def5;

A15: now :: thesis: ( v in the carrier' of G1 implies ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) )

assume A16: v in the carrier' of G1 ; :: thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v )
then A17: the Source of G3 . v = the Source of G1 . v by A6, Def18
.= the Source of (G1 \/ G2) . v by A4, A16, Def5 ;
the Target of G3 . v = the Target of G1 . v by A6, A16, Def18
.= the Target of (G1 \/ G2) . v by A4, A16, Def5 ;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A17; :: thesis: verum

end;

now :: thesis: ( v in the carrier' of G2 implies ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) )

assume A18: v in the carrier' of G2 ; :: thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v )
then A19: the Source of G3 . v = the Source of G2 . v by A7, Def18
.= the Source of (G1 \/ G2) . v by A4, A18, Def5 ;
the Target of G3 . v = the Target of G2 . v by A7, A18, Def18
.= the Target of (G1 \/ G2) . v by A4, A18, Def5 ;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A19; :: thesis: verum

end;

hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A14, A15, XBOOLE_0:def 3; :: thesis: verum

end;

hence the Source of G3 . v in the carrier of (G1 \/ G2) by A12, FUNCT_2:5; :: thesis: the Target of G3 . v in the carrier of (G1 \/ G2)
thus the Target of G3 . v in the carrier of (G1 \/ G2) by A12, A13, FUNCT_2:5; :: thesis: verum

end;

hence ( the carrier of G c= the carrier of G3 & the carrier' of G c= the carrier' of G3 & ( for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G3 . v & the Target of G . v = the Target of G3 . v & the Source of G3 . v in the carrier of G & the Target of G3 . v in the carrier of G ) ) ) by A4, A5, A9, A11, Def5; :: according to GRAPH_1:def 18,GRAPH_1:def 24 :: thesis: verum