set v = the Vertex of G;
reconsider S = { the Vertex of G} as Subset of (the_Vertices_of G) ;
take S ; :: thesis: ( not S is empty & S is proper )
S <> the_Vertices_of G

proof

assume S = the_Vertices_of G ; :: thesis: contradiction
then card (the_Vertices_of G) = 1 by CARD_1:30;
hence contradiction by Def19; :: thesis: verum

end;

hence ( not S is empty & S is proper ) by SUBSET_1:def 6; :: thesis: verum