let C be Subset of R; ( C is 1 -element implies C is strong-chain )
assume
C is 1 -element
; 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; DILWORTH:def 13 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
; ( 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; 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
;
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
;
( 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;
( S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )thus
S /\ C c= c
for d being set st d in P & d <> c holds
C /\ d = {} let d be
set ;
( d in P & d <> c implies C /\ d = {} )assume that A6:
d in P
and A7:
d <> c
;
C /\ d = {} assume
C /\ d <> {}
;
contradictionthen 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;
verum end; end;