let X be set ; 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; 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 ; 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 ; ( 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
; 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; ( v <> w implies ex e being set st
( e in the SEdges of g & e = {v,w} ) )
assume A4:
v <> w
; ex e being set st
( e in the SEdges of g & e = {v,w} )
take
{v,w}
; ( {v,w} in the SEdges of g & {v,w} = {v,w} )
hereby {v,w} = {v,w}
end;
thus
{v,w} = {v,w}
; verum