let X be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( v in the carrier of g implies ex VV being finite set st
( VV = the carrier of g & degree g,v < card VV ) )
assume A1: v in the carrier of g ; :: thesis: 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 Th27;
take VV ; :: thesis: ( VV = the carrier of g & degree g,v < card VV )
consider ww being finite set such that
A2: ( ww = { w where w is Element of X : ( w in VV & {v,w} in the SEdges of g ) } & degree g,v = card ww ) by Th39;
A3: ww c= VV

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in ww or e in VV )
assume e in ww ; :: thesis: e in VV
then consider w being Element of X such that
A4: ( e = w & w in VV & {v,w} in the SEdges of g ) by A2;
thus e in VV by A4; :: thesis: verum

end;

now

assume ww = VV ; :: thesis: ww <> VV
then consider w being Element of X such that
A5: ( v = w & w in VV & {v,w} in the SEdges of g ) by A1, A2;
{v,v} = {v} by ENUMSET1:69;
then consider x, y being set such that
A6: ( x in VV & y in VV & x <> y & {v} = {x,y} ) by A5, Th10;
( v = x & v = y ) by A6, ZFMISC_1:8;
hence ww <> VV by A6; :: thesis: verum

end;

then ww c< VV by A3, XBOOLE_0:def 8;
hence ( VV = the carrier of g & degree g,v < card VV ) by A2, CARD_2:67; :: thesis: verum