let X be non empty set ; for g being SimpleGraph of X
for v being set st v in the carrier of g holds
ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV )
let g be SimpleGraph of X; for v being set st v in the carrier of g holds
ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV )
let v be set ; ( v in the carrier of g implies ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV ) )
reconsider VV = the carrier of g as finite set by Th21;
consider ww being finite set such that
A1:
ww = { w where w is Element of X : ( w in VV & {v,w} in the SEdges of g ) }
and
A2:
degree (g,v) = card ww
by Th28;
assume A3:
v in the carrier of g
; ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV )
A4:
now ( ww = VV implies ww <> VV )end;
take
VV
; ( VV = the carrier of g & degree (g,v) < card VV )
ww c= VV
then
ww c< VV
by A4, XBOOLE_0:def 8;
hence
( VV = the carrier of g & degree (g,v) < card VV )
by A2, CARD_2:48; verum