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 GLIB_000:def 19; :: thesis: verum
end;
hence ( not S is empty & S is proper ) by SUBSET_1:def 6; :: thesis: verum