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 & G2 c= G & G3 c= G ) ; :: thesis: (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)
( the Source of G1 c= the Source of G & the Source of G2 c= the Source of G & the Source of G3 c= the Source of G & the Target of G1 c= the Target of G & the Target of G2 c= the Target of G & the Target of G3 c= the Target of G ) by A1, Th5;
then ( the Source of G1 tolerates the Source of G2 & the Source of G1 tolerates the Source of G3 & the Source of G2 tolerates the Source of G3 & the Target of G1 tolerates the Target of G2 & the Target of G1 tolerates the Target of G3 & the Target of G2 tolerates the Target of G3 ) by PARTFUN1:139;
hence (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) by Th9; :: thesis: verum