let G be non _trivial _Graph; :: thesis: for v being Vertex of G holds not (the_Vertices_of G) \ {v} is empty
let v be Vertex of G; :: thesis: not (the_Vertices_of G) \ {v} is empty
set VG = the_Vertices_of G;
now :: thesis: not (the_Vertices_of G) \ {v} = {}
assume (the_Vertices_of G) \ {v} = {} ; :: thesis: contradiction
then the_Vertices_of G c= {v} by XBOOLE_1:37;
then the_Vertices_of G = {v} by ZFMISC_1:33;
then card (the_Vertices_of G) = 1 by CARD_1:30;
hence contradiction by Def19; :: thesis: verum
end;
hence not (the_Vertices_of G) \ {v} is empty ; :: thesis: verum