let G1, G2, G3 be Graph; :: thesis: ( ex G being Graph st
( G1 c= G & G2 c= G & G3 c= G ) implies (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) )
given G being Graph such that A1: G1 c= G and
A2: G2 c= G and
A3: G3 c= G ; :: thesis: (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)
A4: the Source of G1 c= the Source of G by A1, Th5;
A5: the Source of G2 c= the Source of G by A2, Th5;
A6: the Source of G3 c= the Source of G by A3, Th5;
A7: the Target of G1 c= the Target of G by A1, Th5;
A8: the Target of G2 c= the Target of G by A2, Th5;
A9: the Target of G3 c= the Target of G by A3, Th5;
A10: the Source of G1 tolerates the Source of G2 by A4, A5, PARTFUN1:57;
A11: the Source of G1 tolerates the Source of G3 by A4, A6, PARTFUN1:57;
A12: the Source of G2 tolerates the Source of G3 by A5, A6, PARTFUN1:57;
A13: the Target of G1 tolerates the Target of G2 by A7, A8, PARTFUN1:57;
A14: the Target of G1 tolerates the Target of G3 by A7, A9, PARTFUN1:57;
the Target of G2 tolerates the Target of G3 by A8, A9, PARTFUN1:57;
hence (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) by A10, A11, A12, A13, A14, Th9; :: thesis: verum