let C be Subset of R; :: thesis: ( C is 1 -element implies C is strong-chain )
assume C is 1 -element ; :: thesis: C is strong-chain
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: 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
A2: card P = stability# (subrelstr S) by Th51;
A3: 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 A2, Th44; :: 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 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: ( 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 A5; :: 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 object ; :: 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 A4, A1, TARSKI:def 1; :: thesis: verum

end;

let d be set ; :: thesis: ( d in P & d <> c implies C /\ d = {} )
assume that
A6: d in P and
A7: d <> c ; :: thesis: C /\ d = {}
assume C /\ d <> {} ; :: thesis: contradiction
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: verum

end;

suppose A9: 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 = {} ) )

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

end;

end;