let X be set ; :: thesis: for g being SimpleGraph of X
for v, e being set st 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 e in the SEdges of g & degree (g,v) = 0 holds
not v in e
let v, e be set ; :: thesis: ( e in the SEdges of g & degree (g,v) = 0 implies not v in e )
assume that
A1: e in the SEdges of g and
A2: degree (g,v) = 0 ; :: thesis: not v in e
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 ) ) and
A4: degree (g,v) = card Y by Def8;
assume v in e ; :: thesis: contradiction
then not Y is empty by A1, A3;
hence contradiction by A2, A4; :: thesis: verum