set cR = the carrier of R;
per cases ( R is empty or not R is empty ) ;
suppose R is empty ; :: thesis: ex b1 being a_partition of the carrier of R st b1 is StableSet-wise
then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
take S ; :: thesis: S is StableSet-wise
let x be set ; :: according to DILWORTH:def 12 :: thesis: ( x in S implies x is StableSet of R )
thus ( x in S implies x is StableSet of R ) ; :: thesis: verum
end;
suppose A1: not R is empty ; :: thesis: ex b1 being a_partition of the carrier of R st b1 is StableSet-wise
then reconsider RR = R as non empty RelStr ;
take S = SmallestPartition the carrier of R; :: thesis: S is StableSet-wise
let z be set ; :: according to DILWORTH:def 12 :: thesis: ( z in S implies z is StableSet of R )
assume A2: z in S ; :: thesis: z is StableSet of R
S = { {x} where x is Element of the carrier of R : verum } by A1, EQREL_1:37;
then consider x being Element of RR such that
A3: z = {x} by A2;
thus z is StableSet of R by A3; :: thesis: verum
end;
end;