let G2 be removeEdges of G,X; :: thesis: not G2 is _trivial
ex v1, v2 being Vertex of G2 st v1 <> v2

proof

consider v1, v2 being Vertex of G such that
A1: v1 <> v2 by Th21;
reconsider v1 = v1, v2 = v2 as Vertex of G2 by Th53;
take v1 ; :: thesis: ex v2 being Vertex of G2 st v1 <> v2
take v2 ; :: thesis: v1 <> v2
thus v1 <> v2 by A1; :: thesis: verum

end;

hence not G2 is _trivial by Th116; :: thesis: verum