set cR = the carrier of R;

per cases ( R is empty or not R is empty ) ;

suppose R is empty ; :: thesis: ex b₁ being a_partition of the carrier of R st b₁ 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 b₁ being a_partition of the carrier of R st b₁ 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;