let G be SimpleGraph; :: thesis: for x, y being set st x in Vertices G & y in Vertices G & {x,y} nin G holds
{x,y} is StableSet of G
let x, y be set ; :: thesis: ( x in Vertices G & y in Vertices G & {x,y} nin G implies {x,y} is StableSet of G )
assume that
A1: x in Vertices G and
A2: y in Vertices G and
A3: {x,y} nin G ; :: thesis: {x,y} is StableSet of G
reconsider S = {x,y} as Subset of (Vertices G) by A1, A2, ZFMISC_1:32;
S is stable
proof
let a, b be set ; :: according to SCMYCIEL:def 19 :: thesis: ( a <> b & a in S & b in S implies {a,b} nin G )
assume that
A4: a <> b and
A5: a in S and
A6: b in S ; :: thesis: {a,b} nin G
( ( a = x or a = y ) & ( b = x or b = y ) ) by A5, A6, TARSKI:def 2;
hence {a,b} nin G by A3, A4; :: thesis: verum
end;
hence {x,y} is StableSet of G ; :: thesis: verum