let G be SimpleGraph; :: thesis: for S being Subset of (Vertices G)
for v being object st S = {v} holds
S is stable
let S be Subset of (Vertices G); :: thesis: for v being object st S = {v} holds
S is stable
let v be object ; :: thesis: ( S = {v} implies S is stable )
assume A1: S = {v} ; :: thesis: S is stable
let x, y be set ; :: according to SCMYCIEL:def 19 :: thesis: ( x <> y & x in S & y in S implies {x,y} nin G )
assume that
A2: x <> y and
A3: ( x in S & y in S ) ; :: thesis: {x,y} nin G
( x = v & y = v ) by A1, A3, TARSKI:def 1;
hence {x,y} nin G by A2; :: thesis: verum