let G be SimpleGraph; :: thesis: SmallestPartition (Vertices G) is StableSet-wise
set C = SmallestPartition (Vertices G);
let c be set ; :: according to SCMYCIEL:def 20 :: thesis: ( c in SmallestPartition (Vertices G) implies c is StableSet of G )
assume A: c in SmallestPartition (Vertices G) ; :: thesis: c is StableSet of G
consider a being set such that
a in Vertices G and
Ab: c = Class ((id (Vertices G)),a) by A, EQREL_1:def 3;
reconsider cc = c as Subset of (Vertices G) by A;
Z: cc is stable

proof

let x, y be set ; :: according to SCMYCIEL:def 19 :: thesis: ( x <> y & x in cc & y in cc implies {x,y} nin G )
assume that
A1: x <> y and
B1: x in cc and
C1: y in cc ; :: thesis: {x,y} nin G
D1: [a,x] in id (Vertices G) by B1, Ab, RELAT_1:169;
E1: [a,y] in id (Vertices G) by C1, Ab, RELAT_1:169;
E1a: a = y by E1, RELAT_1:def 10;
thus {x,y} nin G by D1, E1a, A1, RELAT_1:def 10; :: thesis: verum

end;

thus c is StableSet of G by Z; :: thesis: verum