let X be set ; :: thesis: for g being SimpleGraph of X
for v, e being set st v in the carrier of g & e in the SEdges of g & degree g,v = 0 holds
not v in e
let g be SimpleGraph of X; :: thesis: for v, e being set st v in the carrier of g & e in the SEdges of g & degree g,v = 0 holds
not v in e
let v, e be set ; :: thesis: ( v in the carrier of g & e in the SEdges of g & degree g,v = 0 implies not v in e )
assume A1: ( v in the carrier of g & e in the SEdges of g & degree g,v = 0 ) ; :: thesis: not v in e
assume A2: v in e ; :: thesis: contradiction
consider Y being finite set such that
A3: ( ( for z being set holds
( z in Y iff ( z in the SEdges of g & v in z ) ) ) & degree g,v = card Y ) by Def11;
not Y is empty by A1, A2, A3;
hence contradiction by A1, A3; :: thesis: verum