let X be set ; :: thesis: for g being SimpleGraph of X
for v being set
for vg being finite set st vg = the carrier of g & v in vg & 1 + (degree (g,v)) = card vg holds
for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} )
let g be SimpleGraph of X; :: thesis: for v being set
for vg being finite set st vg = the carrier of g & v in vg & 1 + (degree (g,v)) = card vg holds
for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} )
let v be set ; :: thesis: for vg being finite set st vg = the carrier of g & v in vg & 1 + (degree (g,v)) = card vg holds
for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} )
let vg be finite set ; :: thesis: ( vg = the carrier of g & v in vg & 1 + (degree (g,v)) = card vg implies for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} ) )
assume that
A1: vg = the carrier of g and
A2: v in vg and
A3: 1 + (degree (g,v)) = card vg ; :: thesis: for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} )
vg is Subset of X by A1, Th21;
then reconsider X = X as non empty set by A2;
let w be Element of vg; :: thesis: ( v <> w implies ex e being set st
( e in the SEdges of g & e = {v,w} ) )
assume A4: v <> w ; :: thesis: ex e being set st
( e in the SEdges of g & e = {v,w} )
take {v,w} ; :: thesis: ( {v,w} in the SEdges of g & {v,w} = {v,w} )

hereby :: thesis: {v,w} = {v,w}

now :: thesis: {v,w} in the SEdges of g

consider ww being finite set such that
A5: ww = { vv where vv is Element of X : ( vv in vg & {v,vv} in the SEdges of g ) } and
A6: degree (g,v) = card ww by A1, Th28;
reconsider wwv = ww \/ {v} as finite set ;
assume A7: not {v,w} in the SEdges of g ; :: thesis: contradiction
A8: ( not v in ww & not w in ww )

proof

hereby :: thesis: not w in ww

assume v in ww ; :: thesis: contradiction
then ex vv being Element of X st
( v = vv & vv in vg & {v,vv} in the SEdges of g ) by A5;
then {v} in the SEdges of g by ENUMSET1:29;
then ex z being finite Subset of vg st
( {v} = z & card z = 2 ) by A1, Th7;
hence contradiction by CARD_1:30; :: thesis: verum

end;

assume w in ww ; :: thesis: contradiction
then ex vv being Element of X st
( w = vv & vv in vg & {v,vv} in the SEdges of g ) by A5;
hence contradiction by A7; :: thesis: verum

end;

A9: now :: thesis: for e being set st e in ww holds
e in vg

let e be set ; :: thesis: ( e in ww implies e in vg )
assume e in ww ; :: thesis: e in vg
then ex vv being Element of X st
( e = vv & vv in vg & {v,vv} in the SEdges of g ) by A5;
hence e in vg ; :: thesis: verum

end;

( wwv c= vg & wwv <> vg )

proof

for e being set st e in {v} holds
e in vg by A2, TARSKI:def 1;
then A10: {v} c= vg by TARSKI:def 3;
ww c= vg by A9, TARSKI:def 3;
hence wwv c= vg by A10, XBOOLE_1:8; :: thesis: wwv <> vg
assume A11: wwv = vg ; :: thesis: contradiction
not w in {v} by A4, TARSKI:def 1;
hence contradiction by A8, A11, XBOOLE_0:def 3; :: thesis: verum

end;

then A12: wwv c< vg by XBOOLE_0:def 8;
card wwv = 1 + (card ww) by A8, CARD_2:41;
hence contradiction by A3, A6, A12, CARD_2:48; :: thesis: verum

end;

hence {v,w} in the SEdges of g ; :: thesis: verum

end;

thus {v,w} = {v,w} ; :: thesis: verum