let R be non empty transitive antisymmetric with_finite_stability# RelStr ; :: thesis: ex S being non empty Subset of R st
( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
set E = { C where C is Subset of R : C is strong-chain } ;
set x = the Element of R;
A1: { the Element of R} in { C where C is Subset of R : C is strong-chain } ;

now :: thesis: for Z being set st Z c= { C where C is Subset of R : C is strong-chain } & Z is c=-linear holds
ex Y being set st
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )

let Z be set ; :: thesis: ( Z c= { C where C is Subset of R : C is strong-chain } & Z is c=-linear implies ex Y being set st
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A2: Z c= { C where C is Subset of R : C is strong-chain } and
A3: Z is c=-linear ; :: thesis: ex Y being set st
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
set Y = union Z;
take Y = union Z; :: thesis: ( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )

now :: thesis: for B being set st B in Z holds
B c= the carrier of R

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

end;

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

proof

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 /\ Y9 c= c & ( for d being set st d in P & d <> c holds
Y9 /\ d = {} ) ) )
set F = S /\ Y;

per cases ( S /\ Y is empty or not S /\ Y is empty ) ;

suppose A4: S /\ Y is empty ; :: thesis: ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds
Y9 /\ d = {} ) ) )

consider p being Clique-partition of (subrelstr S) such that
A5: card p = stability# (subrelstr S) by Th51;
take p ; :: thesis: ( card p <= stability# R & ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) ) )
thus card p <= stability# R by Th44, A5; :: thesis: ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )
set c = the Element of p;
take the Element of p ; :: thesis: ( the Element of p in p & S /\ Y9 c= the Element of p & ( for d being set st d in p & d <> the Element of p holds
Y9 /\ d = {} ) )
thus the Element of p in p ; :: thesis: ( S /\ Y9 c= the Element of p & ( for d being set st d in p & d <> the Element of p holds
Y9 /\ d = {} ) )
thus S /\ Y9 c= the Element of p by A4; :: thesis: for d being set st d in p & d <> the Element of p holds
Y9 /\ d = {}
let d be set ; :: thesis: ( d in p & d <> the Element of p implies Y9 /\ d = {} )
assume that
A6: d in p and
d <> the Element of p ; :: thesis: Y9 /\ d = {}
d c= the carrier of (subrelstr S) by A6;
then d c= S by YELLOW_0:def 15;
hence Y9 /\ d = {} by A4, XBOOLE_1:3, XBOOLE_1:26; :: thesis: verum

end;

suppose A7: not S /\ Y is empty ; :: thesis: ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds
Y9 /\ d = {} ) ) )

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

proof

let x be object ; :: thesis: ( x in S /\ Y implies ex y being object st
( y in Z & S₁[x,y] ) )
assume A10: x in S /\ Y ; :: thesis: ex y being object st
( y in Z & S₁[x,y] )
then x in Y by XBOOLE_0:def 4;
then consider y being set such that
A11: x in y and
A12: y in Z by TARSKI:def 4;
take y ; :: thesis: ( y in Z & S₁[x,y] )
thus ( y in Z & S₁[x,y] ) by A12, A10, A11; :: thesis: verum

end;

consider f being Function of (S /\ Y),Z such that
A13: for x being object st x in S /\ Y holds
S₁[x,f . x] from FUNCT_2:sch 1(A9);
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
A14: m in rng f and
A15: for C being set st C in rng f holds
C c= m by A3, A7, A8, FINSET_1:12, RELAT_1:def 19;
rng f c= Z by RELAT_1:def 19;
then m in Z by A14;
then m in { C where C is Subset of R : C is strong-chain } by A2;
then consider C being Subset of R such that
A16: m = C and
A17: C is strong-chain ;
A18: S /\ Y c= C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S /\ Y or x in C )
assume A19: x in S /\ Y ; :: thesis: x in C
then S₁[x,f . x] by A13;
then A20: x in f . x ;
f . x c= C by A16, A15, A19, A8, FUNCT_2:4;
hence x in C by A20; :: thesis: verum

end;

consider p being Clique-partition of (subrelstr S) such that
A21: card p <= stability# R and
A22: 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 A17;
take p ; :: thesis: ( card p <= stability# R & ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) ) )
thus card p <= stability# R by A21; :: thesis: ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )
consider c being set such that
A23: c in p and
A24: S /\ C c= c and
A25: for d being set st d in p & d <> c holds
C /\ d = {} by A22;
take c ; :: thesis: ( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )
thus c in p by A23; :: thesis: ( S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )
thus S /\ Y9 c= c :: thesis: for d being set st d in p & d <> c holds
Y9 /\ d = {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S /\ Y9 or x in c )
assume x in S /\ Y9 ; :: thesis: x in c
then ( x in S & x in C ) by A18, XBOOLE_0:def 4;
then x in S /\ C by XBOOLE_0:def 4;
hence x in c by A24; :: thesis: verum

end;

let d be set ; :: thesis: ( d in p & d <> c implies Y9 /\ d = {} )
assume that
A26: d in p and
A27: d <> c ; :: thesis: Y9 /\ d = {}
assume Y9 /\ d <> {} ; :: thesis: contradiction
then consider x being object such that
A28: x in Y9 /\ d by XBOOLE_0:def 1;
A29: x in Y9 by A28, XBOOLE_0:def 4;
A30: x in d by A28, XBOOLE_0:def 4;
d is Subset of S by A26, YELLOW_0:def 15;
then x in S /\ Y by A30, A29, XBOOLE_0:def 4;
then x in C /\ d by A30, A18, XBOOLE_0:def 4;
hence contradiction by A26, A27, A25; :: thesis: verum

end;

end;

end;

hence Y in { C where C is Subset of R : C is strong-chain } ; :: thesis: for X1 being set st X1 in Z holds
X1 c= Y
let X1 be set ; :: thesis: ( X1 in Z implies X1 c= Y )
assume A31: X1 in Z ; :: thesis: X1 c= Y
thus X1 c= Y by A31, ZFMISC_1:74; :: thesis: verum

end;

then consider Y being set such that
A32: Y in { C where C is Subset of R : C is strong-chain } and
A33: 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 A1, ORDERS_1:65;
consider C being Subset of R such that
A34: Y = C and
A35: C is strong-chain by A32;
reconsider S = C as non empty Subset of R by A34, A1, A33, XBOOLE_1:2;
take S ; :: thesis: ( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
thus S is strong-chain by A35; :: thesis: for D being Subset of R holds
( not D is strong-chain or not S c< D )
let D be Subset of R; :: thesis: ( not D is strong-chain or not S c< D )
assume that
A36: D is strong-chain and
A37: S c< D ; :: thesis: contradiction
A38: D in { C where C is Subset of R : C is strong-chain } by A36;
( D <> S & S c= D ) by A37;
hence contradiction by A34, A38, A33; :: thesis: verum