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
then A4:
( the
Source of
G1 tolerates the
Source of
G2 & the
Target of
G1 tolerates the
Target of
G2 )
;
A5:
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #)
= G1 \/ G2
by A3;
then
the
carrier of
G = the
carrier of
G1 \/ the
carrier of
G2
by A4, Def5;
then A6:
the
carrier of
G1 c= the
carrier of
G
by XBOOLE_1:7;
the
carrier' of
G = the
carrier' of
G1 \/ the
carrier' of
G2
by A4, A5, Def5;
then A7:
the
carrier' of
G1 c= the
carrier' of
G
by XBOOLE_1:7;
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 )
then
G1 is
Subgraph of
G
by A6, A7, Def18;
hence
G1 c= G
;
verum
end;
hence
G1 c= G
by A1; G2 c= G
thus
G2 c= G
by A1, A2, Th10; verum