let C be Subset of R; :: thesis:
assume C is 1 -element ; :: thesis:
then consider x being object such that
A1: C = {x} by ZFMISC_1:131;
let S be non empty finite Subset of R; :: according to DILWORTH:def 13 :: thesis:
consider P being Clique-partition of (subrelstr S) such that
A2: card P = stability# (subrelstr S) by Th51;
A3: S = the carrier of (subrelstr S) by YELLOW_0:def 15;
take P ; :: thesis:
thus card P <= stability# R by A2, Th44; :: thesis:

suppose x in S ; :: thesis:

then x in union P by A3, EQREL_1:def 4;
then consider c being set such that
A4: x in c and
A5: c in P by TARSKI:def 4;
take c ; :: thesis:
thus c in P by A5; :: thesis:
thus S /\ C c= c :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in S /\ C ; :: thesis:
then a in C by XBOOLE_0:def 4;
hence a in c by A4, A1, TARSKI:def 1; :: thesis:

end;

let d be set ; :: thesis:
assume that
A6: d in P and
A7: d <> c ; :: thesis:
assume C /\ d <> {} ; :: thesis:
then consider a being object such that
A8: a in C /\ d by XBOOLE_0:def 1;
reconsider d = d, c = c as Subset of S by A6, A5, YELLOW_0:def 15;
a in C by A8, XBOOLE_0:def 4;
then a = x by A1, TARSKI:def 1;
then x in d by A8, XBOOLE_0:def 4;
then x in d /\ c by A4, XBOOLE_0:def 4;
then d meets c ;
hence contradiction by A6, A5, A7, EQREL_1:def 4; :: thesis:

end;

suppose A9: not x in S ; :: thesis:

set c = the Element of P;
take the Element of P ; :: thesis:
thus the Element of P in P ; :: thesis:
C misses S by A9, A1, ZFMISC_1:50;
then S /\ C = {} ;
hence S /\ C c= the Element of P ; :: thesis:
let d be set ; :: thesis:
assume that
A10: d in P and
d <> the Element of P ; :: thesis:
not x in d by A9, A3, A10;
then C misses d by A1, ZFMISC_1:50;
hence C /\ d = {} ; :: thesis:

end;

end;