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

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

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

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

end;

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

hence G is edgeless ; :: thesis: verum

end;

end;