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 ) )
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 ; :: thesis: ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV )
A4: now :: thesis: ( ww = VV implies ww <> VV )
assume ww = VV ; :: thesis: ww <> VV
then A5: ex w being Element of X st
( v = w & w in VV & {v,w} in the SEdges of g ) by A3, A1;
{v,v} = {v} by ENUMSET1:29;
then consider x, y being object such that
x in VV and
y in VV and
A6: x <> y and
A7: {v} = {x,y} by A5, Th8;
v = x by A7, ZFMISC_1:4;
hence ww <> VV by A6, A7, ZFMISC_1:4; :: thesis: verum
end;
take VV ; :: thesis: ( VV = the carrier of g & degree (g,v) < card VV )
ww c= VV
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in ww or e in VV )
assume e in ww ; :: thesis: e in VV
then ex w being Element of X st
( e = w & w in VV & {v,w} in the SEdges of g ) by A1;
hence e in VV ; :: thesis: verum
end;
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; :: thesis: verum