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 A1: ( vg = the carrier of g & v in vg & 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} )
then vg is Subset of X by Th27;
then reconsider X = X as non empty set by A1;
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 A2: 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

assume A3: not {v,w} in the SEdges of g ; :: thesis: contradiction
consider ww being finite set such that
A4: ( ww = { vv where vv is Element of X : ( vv in vg & {v,vv} in the SEdges of g ) } & degree g,v = card ww ) by A1, Th39;

A5: now

let e be set ; :: thesis: ( e in ww implies e in vg )
assume e in ww ; :: thesis: e in vg
then consider vv being Element of X such that
A6: ( e = vv & vv in vg & {v,vv} in the SEdges of g ) by A4;
thus e in vg by A6; :: thesis: verum

end;

A7: ( not v in ww & not w in ww )

proof

hereby :: thesis: not w in ww

assume v in ww ; :: thesis: contradiction
then consider vv being Element of X such that
A8: ( v = vv & vv in vg & {v,vv} in the SEdges of g ) by A4;
{v} in the SEdges of g by A8, ENUMSET1:69;
then consider z being finite Subset of vg such that
A9: ( {v} = z & card z = 2 ) by A1, Th9;
thus contradiction by A9, CARD_1:50; :: thesis: verum

end;

assume w in ww ; :: thesis: contradiction
then consider vv being Element of X such that
A10: ( w = vv & vv in vg & {v,vv} in the SEdges of g ) by A4;
thus contradiction by A3, A10; :: thesis: verum

end;

reconsider wwv = ww \/ {v} as finite set ;
A11: card wwv = 1 + (card ww) by A7, CARD_2:54;
( wwv c= vg & wwv <> vg )

proof

A12: ww c= vg by A5, TARSKI:def 3;
for e being set st e in {v} holds
e in vg by A1, TARSKI:def 1;
then {v} c= vg by TARSKI:def 3;
hence wwv c= vg by A12, XBOOLE_1:8; :: thesis: wwv <> vg
A13: not w in {v} by A2, TARSKI:def 1;
assume wwv = vg ; :: thesis: contradiction
hence contradiction by A7, A13, XBOOLE_0:def 3; :: thesis: verum

end;

then wwv c< vg by XBOOLE_0:def 8;
hence contradiction by A1, A4, A11, CARD_2:67; :: thesis: verum

end;

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

end;

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