let G be GraphUnion of G1,G2; :: thesis: G is loopfull

per cases ( G1 tolerates G2 or not G1 tolerates G2 ) ;

suppose G1 tolerates G2 ; :: thesis: G is loopfull

then consider S being GraphUnionSet such that
A1: ( S = {G1,G2} & G is GraphUnion of S ) by Def26;
thus G is loopfull by A1; :: thesis: verum

end;

suppose not G1 tolerates G2 ; :: thesis: G is loopfull

then G1 == G by Def26;
hence G is loopfull by GLIB_012:4; :: thesis: verum

end;

end;