let G be _Graph; :: thesis: ( ex v1, v2 being Vertex of G st v1 <> v2 implies not G is trivial )
given v1, v2 being Vertex of G such that A1: v1 <> v2 ; :: thesis: not G is trivial
card (the_Vertices_of G) <> 1

proof

assume card (the_Vertices_of G) = 1 ; :: thesis: contradiction
then card {v1,v2} c= 1 by CARD_1:11;
then {0,1} c= 1 by A1, CARD_2:57, CARD_1:50;
then 1 in 1 by ZFMISC_1:32;
hence contradiction ; :: thesis: verum

end;

hence not G is trivial by GLIB_000:def 19; :: thesis: verum