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 Clique-wise

then reconsider S = {} as a_partition of the carrier of R by EQREL_1:54;
take S ; :: thesis: S is Clique-wise
thus for x being set st x in S holds
x is Clique of R ; :: according to DILWORTH:def 11 :: thesis: verum

end;

suppose S: not R is empty ; :: thesis: ex b₁ being a_partition of the carrier of R st b₁ is Clique-wise

take S = SmallestPartition the carrier of R; :: thesis: S is Clique-wise
let z be set ; :: according to DILWORTH:def 11 :: thesis: ( z in S implies z is Clique of R )
assume A: z in S ; :: thesis: z is Clique of R
S = { {x} where x is Element of the carrier of R : verum } by S, EQREL_1:46;
then consider x being Element of the carrier of R such that
B: z = {x} and
verum by A;
thus z is Clique of R by B, S, SUBSET_1:55; :: thesis: verum

end;

end;