let R be non empty transitive antisymmetric with_finite_stability# RelStr ; :: thesis:
set E = { C where C is Subset of R : C is strong-chain } ;
consider x being Element of R;
reconsider xs = {x} as Subset of R ;
Aa: {x} in { C where C is Subset of R : C is strong-chain } ;

let Z be set ; :: thesis:
assume that
A1: Z c= { C where C is Subset of R : C is strong-chain } and
B1: Z is c=-linear ; :: thesis:
set Y = union Z;
take Y = union Z; :: thesis:

let B be set ; :: thesis:
assume B in Z ; :: thesis:
then B in { C where C is Subset of R : C is strong-chain } by A1;
then ex C being Subset of R st
( C = B & C is strong-chain ) ;
hence B c= the carrier of R ; :: thesis:

end;

then reconsider Y9 = Y as Subset of R by ZFMISC_1:94;
Y9 is strong-chain

let S be non empty finite Subset of R; :: according to DILWORTH:def 13 :: thesis:
set F = S /\ Y;

end;

then S1a: not Z is empty by ZFMISC_1:2;
defpred S₁[ set , set ] means ( $1 in S /\ Y & $2 in Z & $1 in $2 );
P: for x being set st x in S /\ Y holds
ex y being set st
( y in Z & S₁[x,y] )

let x be set ; :: thesis:
assume A4a: x in S /\ Y ; :: thesis:
then x in Y by XBOOLE_0:def 4;
then consider y being set such that
A4: x in y and
B4: y in Z by TARSKI:def 4;
take y ; :: thesis:
thus ( y in Z & S₁[x,y] ) by B4, A4a, A4; :: thesis:

end;

consider f being Function of (S /\ Y),Z such that
J3: for x being set st x in S /\ Y holds
S₁[x,f . x] from FUNCT_2:sch 1(P);
set rf = rng f;
( rng f c= Z & Z is c=-linear implies rng f is c=-linear ) ;
then consider m being set such that
M3: m in rng f and
N3: for C being set st C in rng f holds
C c= m by B1, RELAT_1:def 19, FINSET_1:31, S1, S1a;
rng f c= Z by RELAT_1:def 19;
then m in Z by M3;
then m in { C where C is Subset of R : C is strong-chain } by A1;
then consider C being Subset of R such that
O3: m = C and
P3: C is strong-chain ;
P3a: S /\ Y c= C

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A4: x in S /\ Y ; :: thesis:
then B4: x in f . x by J3;
f . x c= C by O3, N3, A4, S1a, FUNCT_2:6;
hence x in C by B4; :: thesis:

end;

consider p being Clique-partition of (subrelstr S) such that
R3: card p <= stability# R and
S3: 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 = {} ) ) by P3, Lsc;
take p ; :: thesis:
thus card p <= stability# R by R3; :: thesis:
consider c being set such that
T3: c in p and
U3: S /\ C c= c and
V3: for d being set st d in p & d <> c holds
C /\ d = {} by S3;
take c ; :: thesis:
thus c in p by T3; :: thesis:
thus S /\ Y9 c= c :: thesis:

end;

end;

end;

then consider Y being set such that
B: Y in { C where C is Subset of R : C is strong-chain } and
C: for Z being set st Z in { C where C is Subset of R : C is strong-chain } & Z <> Y holds
not Y c= Z by Aa, ORDERS_1:175;
consider C being Subset of R such that
D: Y = C and
E: C is strong-chain by B;
reconsider S = C as non empty Subset of R by D, Aa, C, XBOOLE_1:2;
take S ; :: thesis:
thus S is strong-chain by E; :: thesis:
let D be Subset of R; :: thesis:
assume that
F: D is strong-chain and
G: S c< D ; :: thesis:
I: D in { C where C is Subset of R : C is strong-chain } by F;
( D <> S & S c= D ) by G, XBOOLE_0:def 8;
hence contradiction by D, I, C; :: thesis: