let G, G1, G2 be Graph; ( G is_sum_of G1,G2 implies ( G1 c= G & G2 c= G ) )
assume A1:
G is_sum_of G1,G2
; ( G1 c= G & G2 c= G )
A2:
for G, G1, G2 being Graph st G is_sum_of G1,G2 holds
G1 c= G
proof
let G,
G1,
G2 be
Graph;
( G is_sum_of G1,G2 implies G1 c= G )
assume A3:
G is_sum_of G1,
G2
;
G1 c= G
A4:
( the
Source of
G1 tolerates the
Source of
G2 & the
Target of
G1 tolerates the
Target of
G2 )
by A3, Def4;
A5:
MultiGraphStruct(# the
carrier of
G,the
carrier' of
G,the
Source of
G,the
Target of
G #)
= G1 \/ G2
by A3, Def4;
A6:
the
carrier of
G = the
carrier of
G1 \/ the
carrier of
G2
by A4, A5, Def3;
A7:
the
carrier of
G1 c= the
carrier of
G
by A6, XBOOLE_1:7;
A8:
the
carrier' of
G = the
carrier' of
G1 \/ the
carrier' of
G2
by A4, A5, Def3;
A9:
the
carrier' of
G1 c= the
carrier' of
G
by A8, XBOOLE_1:7;
A10:
for
v being
set st
v in the
carrier' of
G1 holds
( the
Source of
G1 . v = the
Source of
G . v & the
Target of
G1 . v = the
Target of
G . v & the
Source of
G . v in the
carrier of
G1 & the
Target of
G . 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 G . v & the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 ) )
assume A11:
v in the
carrier' of
G1
;
( the Source of G1 . v = the Source of G . v & the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 )
thus A12:
the
Source of
G1 . v = the
Source of
G . v
by A4, A5, A11, Def3;
( the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 )
thus A13:
the
Target of
G1 . v = the
Target of
G . v
by A4, A5, A11, Def3;
( the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 )
thus
the
Source of
G . v in the
carrier of
G1
by A11, A12, FUNCT_2:7;
the Target of G . v in the carrier of G1
thus
the
Target of
G . v in the
carrier of
G1
by A11, A13, FUNCT_2:7;
verum
end;
A14:
G1 is
Subgraph of
G
by A7, A9, A10, Def18;
thus
G1 c= G
by A14, Def24;
verum
end;
thus
G1 c= G
by A1, A2; G2 c= G
thus
G2 c= G
by A1, A2, Th10; verum