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

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

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

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

end;

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

then G1 == G by Def26;
hence G is loopless by GLIB_000:89; :: thesis: verum

end;

end;