let G be SimpleGraph; :: thesis: {} (Vertices G) is stable
let x, y be set ; :: according to SCMYCIEL:def 19 :: thesis: ( x <> y & x in {} (Vertices G) & y in {} (Vertices G) implies {x,y} nin G )
assume that
x <> y and
A: x in {} (Vertices G) and
y in {} (Vertices G) ; :: thesis: {x,y} nin G
thus {x,y} nin G by A; :: thesis: verum