Nuprl - graph_1_3 LEMMAs for vertex_DASH_count_DASH

Rank	Theorem	Name
8	Thm* For any graph the_obj:GraphObject(the_graph), P,Q:(V). (x:V. P(x) Q(x)) (x:V. P(x) & Q(x)) vertex-count(the_obj;x.P(x)) < vertex-count(the_obj;x.Q(x))	[vertex-count-less]
cites
2	Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) (x:T. (x A) & (x B)) \|\|A\|\| < \|\|B\|\|	[length_less]
7	Thm* For any graph the_obj:GraphObject(the_graph), P:(V). no_repeats(V;vertex-subset(the_obj;x.P(x))) & (x:V. (x vertex-subset(the_obj;x.P(x))) P(x))	[vertex-subset-properties]