let G be non _trivial _Graph; :: thesis: ex v1, v2 being Vertex of G st v1 <> v2
set VG = the_Vertices_of G;
take v1 = the Element of the_Vertices_of G; :: thesis: ex v2 being Vertex of G st v1 <> v2
set VG2 = (the_Vertices_of G) \ {v1};
now :: thesis: not (the_Vertices_of G) \ {v1} = {}
assume A1: (the_Vertices_of G) \ {v1} = {} ; :: thesis: contradiction
card (((the_Vertices_of G) \ {v1}) \/ {v1}) = (card ((the_Vertices_of G) \ {v1})) +` (card {v1}) by CARD_2:35, XBOOLE_1:79
.= 0 +` 1 by A1, CARD_1:30
.= card (0 +^ 1) by CARD_2:def 1
.= card (0 + 1) by CARD_2:36
.= 1 ;
then card (the_Vertices_of G) = 1 by XBOOLE_1:45;
hence contradiction by Def19; :: thesis: verum
end;
then reconsider VG2 = (the_Vertices_of G) \ {v1} as non empty set ;
set v2 = the Element of VG2;
A2: not the Element of VG2 in {v1} by XBOOLE_0:def 5;
reconsider v2 = the Element of VG2 as Vertex of G by XBOOLE_0:def 5;
take v2 ; :: thesis: v1 <> v2
thus v1 <> v2 by A2, TARSKI:def 1; :: thesis: verum