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

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] ) 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 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 = {} 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