let G be SimpleGraph; SmallestPartition (Vertices G) is StableSet-wise
set C = SmallestPartition (Vertices G);
let c be set ; SCMYCIEL:def 20 ( c in SmallestPartition (Vertices G) implies c is StableSet of G )
assume A1:
c in SmallestPartition (Vertices G)
; 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 ;
SCMYCIEL:def 19 ( 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
;
{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;
verum
end;
thus
c is StableSet of G
by A3; verum