let G1, G, G2 be Graph; :: thesis: ( G1 c= G & G2 c= G implies G1 \/ G2 c= G )
assume A1: ( G1 c= G & G2 c= G ) ; :: thesis: G1 \/ G2 c= G
A2: ( the Source of G1 c= the Source of G & the Source of G2 c= the Source of G ) by A1, Th5;
A3: ( the Target of G1 c= the Target of G & the Target of G2 c= the Target of G ) by A1, Th5;
A4: the Source of G1 tolerates the Source of G2 by A2, PARTFUN1:139;
A5: the Target of G1 tolerates the Target of G2 by A3, PARTFUN1:139;
A6: G1 \/ G2 is_sum_of G1,G2 by A4, A5, Def4;
thus G1 \/ G2 c= G by A1, A6, Th21; :: thesis: verum