let C be Subset of R; :: thesis: ( C is trivial & not C is empty implies C is strong-chain )
assume ( C is trivial & not C is empty ) ; :: thesis: C is strong-chain
then consider x being set such that
Z: C = {x} by REALSET1:def 4;
let S be non empty finite Subset of R; :: according to DILWORTH:def 13 :: thesis: ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) )
consider P being Clique-partition of (subrelstr S) such that
A1: card P = stability# (subrelstr S) by DWf;
cS: S = the carrier of (subrelstr S) by YELLOW_0:def 15;
take P ; :: thesis: ( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) )
thus card P <= stability# R by A1, Wsubp0; :: thesis: ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )

per cases ( x in S or not x in S ) ;

suppose x in S ; :: thesis: ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )

then x in union P by cS, EQREL_1:def 6;
then consider c being set such that
A2: x in c and
B2: c in P by TARSKI:def 4;
take c ; :: thesis: ( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
thus c in P by B2; :: thesis: ( S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
thus S /\ C c= c :: thesis: for d being set st d in P & d <> c holds
C /\ d = {}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in S /\ C or a in c )
assume a in S /\ C ; :: thesis: a in c
then a in C by XBOOLE_0:def 4;
hence a in c by A2, Z, TARSKI:def 1; :: thesis: verum

end;

let d be set ; :: thesis: ( d in P & d <> c implies C /\ d = {} )
assume that
C3: d in P and
D3: d <> c ; :: thesis: C /\ d = {}
assume C /\ d <> {} ; :: thesis: contradiction
then consider a being set such that
E3: a in C /\ d by XBOOLE_0:def 1;
reconsider d = d, c = c as Subset of S by C3, B2, YELLOW_0:def 15;
a in C by E3, XBOOLE_0:def 4;
then a = x by Z, TARSKI:def 1;
then x in d by E3, XBOOLE_0:def 4;
then x in d /\ c by A2, XBOOLE_0:def 4;
then d meets c by XBOOLE_0:def 7;
hence contradiction by C3, B2, D3, EQREL_1:def 6; :: thesis: verum

end;

suppose S1: not x in S ; :: thesis: ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )

consider c being Element of P;
take c ; :: thesis: ( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
thus c in P ; :: thesis: ( S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
C misses S by S1, ZFMISC_1:56, Z;
then S /\ C = {} by XBOOLE_0:def 7;
hence S /\ C c= c by XBOOLE_1:2; :: thesis: for d being set st d in P & d <> c holds
C /\ d = {}
let d be set ; :: thesis: ( d in P & d <> c implies C /\ d = {} )
assume that
A2: d in P and
d <> c ; :: thesis: C /\ d = {}
not x in d by S1, cS, A2;
then C misses d by ZFMISC_1:56, Z;
hence C /\ d = {} by XBOOLE_0:def 7; :: thesis: verum

end;

end;