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:45;
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 A1: 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 A2: z in S ; :: thesis: z is Clique of R
S = { {x} where x is Element of the carrier of R : verum } by A1, EQREL_1:37;
then ex x being Element of the carrier of R st z = {x} by A2;
hence z is Clique of R by A1, SUBSET_1:33; :: thesis: verum

end;

end;