let G1, G3, G2, G be Graph; :: thesis: ( G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 implies G c= G3 )
assume A1: ( G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 ) ; :: thesis: G c= G3
then A2: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by Def3;
A3: MultiGraphStruct(# the carrier of G,the carrier' of G,the Source of G,the Target of G #) = G1 \/ G2 by A1, Def3;
A4: G1 is Subgraph of G3 by A1, Def23;
A5: G2 is Subgraph of G3 by A1, Def23;
then ( the carrier of G1 c= the carrier of G3 & the carrier of G2 c= the carrier of G3 ) by A4, Def17;
then A6: the carrier of G1 \/ the carrier of G2 c= the carrier of G3 by XBOOLE_1:8;
( the carrier' of G1 c= the carrier' of G3 & the carrier' of G2 c= the carrier' of G3 ) by A4, A5, Def17;
then A7: the carrier' of G1 \/ the carrier' of G2 c= the carrier' of G3 by 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 A8: 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 A9: ( 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

A10: v in the carrier' of G1 \/ the carrier' of G2 by A2, A8, Def2;

A11: now

assume A12: 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 A13: the Source of G3 . v = the Source of G1 . v by A4, Def17
.= the Source of (G1 \/ G2) . v by A2, A12, Def2 ;
the Target of G3 . v = the Target of G1 . v by A4, A12, Def17
.= the Target of (G1 \/ G2) . v by A2, A12, Def2 ;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A13; :: thesis: verum

end;

now

assume A14: 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 A15: the Source of G3 . v = the Source of G2 . v by A5, Def17
.= the Source of (G1 \/ G2) . v by A2, A14, Def2 ;
the Target of G3 . v = the Target of G2 . v by A5, A14, Def17
.= the Target of (G1 \/ G2) . v by A2, A14, Def2 ;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A15; :: 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 A10, A11, XBOOLE_0:def 3; :: thesis: verum

end;

hence the Source of G3 . v in the carrier of (G1 \/ G2) by A8, FUNCT_2:7; :: 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 A8, A9, FUNCT_2:7; :: 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 A2, A3, A6, A7, Def2; :: according to GRAPH_1:def 18,GRAPH_1:def 24 :: thesis: verum