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 A1: c in SmallestPartition (Vertices G) ; :: thesis: c is StableSet of G
consider a being object such that
a in Vertices G and
A2: c = Class ((id (Vertices G)),a) by A1, EQREL_1:def 3;
reconsider cc = c as Subset of (Vertices G) by A1;
A3: 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
A4: x <> y and
A5: x in cc and
A6: y in cc ; :: thesis: {x,y} nin G
A7: [a,x] in id (Vertices G) by A5, A2, RELAT_1:169;
A8: [a,y] in id (Vertices G) by A6, A2, RELAT_1:169;
A9: a = y by A8, RELAT_1:def 10;
thus {x,y} nin G by A7, A9, A4, RELAT_1:def 10; :: thesis: verum

end;

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