let A, N be non empty finite set ; :: thesis:
let f be Function of (Funcs (N,(LinPreorders A))),(LinPreorders A); :: thesis:
assume that
A1: for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds
a <_ f . p,b and
A2: for p, p9 being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds
( ( a <_ p . i,b implies a <_ p9 . i,b ) & ( a <_ p9 . i,b implies a <_ p . i,b ) & ( b <_ p . i,a implies b <_ p9 . i,a ) & ( b <_ p9 . i,a implies b <_ p . i,a ) ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) and
A3: card A >= 3 ; :: thesis:
defpred S₁[ Element of LinPreorders A, Element of A] means ( for a being Element of A st a <> $2 holds
$2 <_ $1,a or for a being Element of A st a <> $2 holds
a <_ $1,$2 );
A4: for p being Element of Funcs (N,(LinPreorders A))
for b being Element of A st ( for i being Element of N holds S₁[p . i,b] ) holds
S₁[f . p,b]

assume ex p being Element of Funcs (N,(LinPreorders A)) ex b being Element of A st
( ( for i being Element of N holds S₁[p . i,b] ) & not S₁[f . p,b] ) ; :: thesis:
then consider p being Element of Funcs (N,(LinPreorders A)), b being Element of A such that
A6: ex a being Element of A st
( a <> b & a <=_ f . p,b ) and
A7: ex c being Element of A st
( c <> b & b <=_ f . p,c ) and
A8: for i being Element of N holds S₁[p . i,b] ;
consider a9 being Element of A such that
A9: ( a9 <> b & a9 <=_ f . p,b ) by A6;
consider c9 being Element of A such that
A10: ( b <> c9 & b <=_ f . p,c9 ) by A7;
ex a, c being Element of A st
( a <> b & b <> c & a <> c & a <=_ f . p,b & b <=_ f . p,c )

suppose A12: a9 <> c9 ; :: thesis:

take a9 ; :: thesis:
take c9 ; :: thesis:
thus ( a9 <> b & b <> c9 & a9 <> c9 & a9 <=_ f . p,b & b <=_ f . p,c9 ) by A9, A10, A12; :: thesis:

end;

suppose A13: a9 = c9 ; :: thesis:

consider d being Element of A such that
A14: ( d <> b & d <> a9 ) by A3, Th2;

per cases by Th4;

suppose A15: d <=_ f . p,b ; :: thesis:

take d ; :: thesis:
take c9 ; :: thesis:
thus ( d <> b & b <> c9 & d <> c9 & d <=_ f . p,b & b <=_ f . p,c9 ) by A10, A13, A14, A15; :: thesis:

end;

suppose A16: b <=_ f . p,d ; :: thesis:

take a9 ; :: thesis:
take d ; :: thesis:
thus ( a9 <> b & b <> d & a9 <> d & a9 <=_ f . p,b & b <=_ f . p,d ) by A9, A14, A16; :: thesis:

end;

end;

end;

end;

end;

then consider a, c being Element of A such that
A17: ( a <> b & b <> c ) and
A18: a <> c and
A19: ( a <=_ f . p,b & b <=_ f . p,c ) ;
defpred S₂[ Element of N, Element of LinPreorders A] means ( ( a <_ p . $1,b implies a <_ $2,b ) & ( a <_ $2,b implies a <_ p . $1,b ) & ( b <_ p . $1,a implies b <_ $2,a ) & ( b <_ $2,a implies b <_ p . $1,a ) & ( b <_ p . $1,c implies b <_ $2,c ) & ( b <_ $2,c implies b <_ p . $1,c ) & ( c <_ p . $1,b implies c <_ $2,b ) & ( c <_ $2,b implies c <_ p . $1,b ) & c <_ $2,a );
A20: for i being Element of N ex o being Element of LinPreorders A st S₂[i,o]

let i be Element of N; :: thesis:

per cases by A8;

suppose for c being Element of A st c <> b holds
b <_ p . i,c ; :: thesis:

then A22: ( b <_ p . i,a & b <_ p . i,c ) by A17;
consider o being Element of LinPreorders A such that
A23: ( b <_ o,c & c <_ o,a ) by A17, A18, Th7;
take o ; :: thesis:
thus S₂[i,o] by A22, A23, Th4, Th5; :: thesis:

end;

suppose for a being Element of A st a <> b holds
a <_ p . i,b ; :: thesis:

then A25: ( a <_ p . i,b & c <_ p . i,b ) by A17;
consider o being Element of LinPreorders A such that
A26: ( c <_ o,a & a <_ o,b ) by A17, A18, Th7;
take o ; :: thesis:
thus S₂[i,o] by A25, A26, Th4, Th5; :: thesis:

end;

end;

end;

consider p9 being Function of N,(LinPreorders A) such that
A27: for i being Element of N holds S₂[i,p9 . i] from FUNCT_2:sch 3(A20);
reconsider p9 = p9 as Element of Funcs (N,(LinPreorders A)) by FUNCT_2:11;
( a <=_ f . p9,b & b <=_ f . p9,c ) by A2, A19, A27;
then a <=_ f . p9,c by Th5;
hence contradiction by A1, A27; :: thesis:

end;

A30: for b being Element of A ex nb being Element of N ex pI, pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S₁[pI . i,b] ) & ( for i being Element of N holds S₁[pII . i,b] ) & ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )

consider t being FinSequence such that
A31: rng t = N and
A32: t is one-to-one by FINSEQ_4:73;
reconsider t = t as FinSequence of N by A31, FINSEQ_1:def 4;
let b be Element of A; :: thesis:
consider oI being Element of LinPreorders A such that
A33: for a being Element of A st a <> b holds
b <_ oI,a by Th8;
consider oII being Element of LinPreorders A such that
A34: for a being Element of A st a <> b holds
a <_ oII,b by Th9;
A35: for k0 being Nat ex p being Element of Funcs (N,(LinPreorders A)) st
( ( for k being Nat st k in dom t & k < k0 holds
p . (t . k) = oII ) & ( for k being Nat st k in dom t & k >= k0 holds
p . (t . k) = oI ) )

let k0 be Nat; :: thesis:
defpred S₂[ Element of N, Element of LinPreorders A] means ex k being Nat st
( k in dom t & $1 = t . k & ( k < k0 implies $2 = oII ) & ( k >= k0 implies $2 = oI ) );
A36: for i being Element of N ex o being Element of LinPreorders A st S₂[i,o]

let i be Element of N; :: thesis:
consider k being set such that
A37: k in dom t and
A38: i = t . k by A31, FUNCT_1:def 5;
reconsider k = k as Nat by A37;

suppose A39: k < k0 ; :: thesis:

take oII ; :: thesis:
thus S₂[i,oII] by A37, A38, A39; :: thesis:

end;

suppose A40: k >= k0 ; :: thesis:

take oI ; :: thesis:
thus S₂[i,oI] by A37, A38, A40; :: thesis:

end;

end;

end;

consider p being Function of N,(LinPreorders A) such that
A41: for i being Element of N holds S₂[i,p . i] from FUNCT_2:sch 3(A36);
reconsider p = p as Element of Funcs (N,(LinPreorders A)) by FUNCT_2:11;
take p ; :: thesis:
thus for k being Nat st k in dom t & k < k0 holds
p . (t . k) = oII :: thesis:

let k be Nat; :: thesis:
assume that
A42: k in dom t and
A43: k < k0 ; :: thesis:
reconsider i = t . k as Element of N by A42, PARTFUN1:27;
S₂[i,p . i] by A41;
hence p . (t . k) = oII by A32, A42, A43, FUNCT_1:def 8; :: thesis:

end;

let k be Nat; :: thesis:
assume that
A45: k in dom t and
A46: k >= k0 ; :: thesis:
reconsider i = t . k as Element of N by A45, PARTFUN1:27;
S₂[i,p . i] by A41;
hence p . (t . k) = oI by A32, A45, A46, FUNCT_1:def 8; :: thesis:

end;

defpred S₂[ Nat] means for p being Element of Funcs (N,(LinPreorders A)) st ( for k being Nat st k in dom t & k < $1 holds
p . (t . k) = oII ) & ( for k being Nat st k in dom t & k >= $1 holds
p . (t . k) = oI ) holds
for a being Element of A st a <> b holds
a <_ f . p,b;
reconsider kII9 = (len t) + 1 as Element of NAT by ORDINAL1:def 13;
A48: S₂[kII9]

let p be Element of Funcs (N,(LinPreorders A)); :: thesis:
assume that
A49: for k being Nat st k in dom t & k < kII9 holds
p . (t . k) = oII and
for k being Nat st k in dom t & k >= kII9 holds
p . (t . k) = oI ; :: thesis:
let a be Element of A; :: thesis:
assume A50: a <> b ; :: thesis:
for i being Element of N holds a <_ p . i,b

let i be Element of N; :: thesis:
consider k being set such that
A52: k in dom t and
A53: i = t . k by A31, FUNCT_1:def 5;
reconsider k = k as Nat by A52;
k <= len t by A52, FINSEQ_3:27;
then k + 0 < kII9 by XREAL_1:10;
then p . i = oII by A49, A52, A53;
hence a <_ p . i,b by A34, A50; :: thesis:

end;

hence a <_ f . p,b by A1; :: thesis:

end;

then A57: ex kII9 being Nat st S₂[kII9] ;
consider kII being Nat such that
A58: ( S₂[kII] & ( for k0 being Nat st S₂[k0] holds
k0 >= kII ) ) from NAT_1:sch 5(A57);
consider pII being Element of Funcs (N,(LinPreorders A)) such that
A59: for k being Nat st k in dom t & k < kII holds
pII . (t . k) = oII and
A60: for k being Nat st k in dom t & k >= kII holds
pII . (t . k) = oI by A35;
A61: kII > 1

assume A62: kII <= 1 ; :: thesis:
consider a being Element of A such that
A63: a <> b by A3, Th1, XXREAL_0:2;
A64: for i being Element of N holds b <_ pII . i,a

let i be Element of N; :: thesis:
consider k being set such that
A65: k in dom t and
A66: i = t . k by A31, FUNCT_1:def 5;
reconsider k = k as Nat by A65;
k >= 1 by A65, FINSEQ_3:27;
then pII . i = oI by A60, A62, A65, A66, XXREAL_0:2;
hence b <_ pII . i,a by A33, A63; :: thesis:

end;

A69: a <_ f . pII,b by A58, A59, A60, A63;
b <_ f . pII,a by A1, A64;
hence contradiction by A69, Th4; :: thesis:

end;

then reconsider kI = kII - 1 as Nat by NAT_1:20;
reconsider kI = kI as Element of NAT by ORDINAL1:def 13;
A71: kII = kI + 1 ;
kI > 1 - 1 by A61, XREAL_1:11;
then A73: kI >= 0 + 1 by INT_1:20;
kII <= kII9 by A48, A58;
then kI <= kII9 - 1 by XREAL_1:11;
then A76: kI in dom t by A73, FINSEQ_3:27;
then reconsider nb = t . kI as Element of N by PARTFUN1:27;
A77: kI + 0 < kII by A71, XREAL_1:10;
then consider pI being Element of Funcs (N,(LinPreorders A)) such that
A78: for k being Nat st k in dom t & k < kI holds
pI . (t . k) = oII and
A79: for k being Nat st k in dom t & k >= kI holds
pI . (t . k) = oI and
A80: ex a being Element of A st
( a <> b & not a <_ f . pI,b ) by A58;
take nb ; :: thesis:
take pI ; :: thesis:
take pII ; :: thesis:
thus for i being Element of N st i <> nb holds
pI . i = pII . i :: thesis:

let i be Element of N; :: thesis:
assume A81: i <> nb ; :: thesis:
consider k being set such that
A82: k in dom t and
A83: i = t . k by A31, FUNCT_1:def 5;
reconsider k = k as Nat by A82;

per cases by A81, A83, XXREAL_0:1;

suppose k < kI ; :: thesis:

then ( k + 0 < kII & pI . i = oII ) by A71, A78, A82, A83, XREAL_1:10;
hence pI . i = pII . i by A59, A82, A83; :: thesis:

end;

suppose k > kI ; :: thesis:

then ( k >= kII & pI . i = oI ) by A71, A79, A82, A83, INT_1:20;
hence pI . i = pII . i by A60, A82, A83; :: thesis:

end;

end;

end;

thus A88: for i being Element of N holds S₁[pI . i,b] :: thesis:

let i be Element of N; :: thesis:
ex k being set st
( k in dom t & i = t . k ) by A31, FUNCT_1:def 5;
then ( pI . i = oII or pI . i = oI ) by A78, A79;
hence S₁[pI . i,b] by A33, A34; :: thesis:

end;

thus for i being Element of N holds S₁[pII . i,b] :: thesis:

let i be Element of N; :: thesis:
ex k being set st
( k in dom t & i = t . k ) by A31, FUNCT_1:def 5;
then ( pII . i = oII or pII . i = oI ) by A59, A60;
hence S₁[pII . i,b] by A33, A34; :: thesis:

end;

pI . nb = oI by A76, A79;
hence for a being Element of A st a <> b holds
b <_ pI . nb,a by A33; :: thesis:
pII . nb = oII by A59, A76, A77;
hence for a being Element of A st a <> b holds
a <_ pII . nb,b by A34; :: thesis:
thus for a being Element of A st a <> b holds
b <_ f . pI,a by A4, A80, A88; :: thesis:
thus for a being Element of A st a <> b holds
a <_ f . pII,b by A58, A59, A60; :: thesis:

end;

A95: for b being Element of A ex nb being Element of N ex pI, pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S₁[pI . i,b] ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) & ( for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c ) )

let b be Element of A; :: thesis:
consider nb being Element of N, pI, pII being Element of Funcs (N,(LinPreorders A)) such that
A96: for i being Element of N st i <> nb holds
pI . i = pII . i and
A97: for i being Element of N holds S₁[pI . i,b] and
A98: for i being Element of N holds S₁[pII . i,b] and
A99: for a being Element of A st a <> b holds
b <_ pI . nb,a and
A100: for a being Element of A st a <> b holds
a <_ pII . nb,b and
A101: ( ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) ) by A30;
take nb ; :: thesis:
take pI ; :: thesis:
take pII ; :: thesis:
thus ( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S₁[pI . i,b] ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) ) by A96, A97, A101; :: thesis:
let p be Element of Funcs (N,(LinPreorders A)); :: thesis:
let a, c be Element of A; :: thesis:
assume that
A102: a <> b and
A103: c <> b and
A104: a <_ p . nb,c ; :: thesis:
A105: a <> c by A104, Th3;
defpred S₂[ Element of N, Element of LinPreorders A] means ( ( a <_ p . $1,c implies a <_ $2,c ) & ( a <_ $2,c implies a <_ p . $1,c ) & ( c <_ p . $1,a implies c <_ $2,a ) & ( c <_ $2,a implies c <_ p . $1,a ) & ( $1 = nb implies ( a <_ $2,b & b <_ $2,c ) ) & ( $1 <> nb implies ( ( ( for d being Element of A st d <> b holds
b <_ pII . $1,d ) implies ( b <_ $2,a & b <_ $2,c ) ) & ( ( for d being Element of A st d <> b holds
d <_ pII . $1,b ) implies ( a <_ $2,b & c <_ $2,b ) ) ) ) );
A106: for i being Element of N ex o being Element of LinPreorders A st S₂[i,o]

let i be Element of N; :: thesis:

suppose A107: i = nb ; :: thesis:

consider o being Element of LinPreorders A such that
A108: ( a <_ o,b & b <_ o,c ) by A102, A103, A105, Th7;
take o ; :: thesis:
thus S₂[i,o] by A104, A107, A108, Th4, Th5; :: thesis:

end;

suppose A109: i <> nb ; :: thesis:

per cases by A98;

suppose for d being Element of A st d <> b holds
b <_ pII . i,d ; :: thesis:

then b <_ pII . i,a by A102;
then A112: not a <_ pII . i,b by Th4;
consider o being Element of LinPreorders A such that
A113: ( b <_ o,a & b <_ o,c & ( a <_ o,c implies a <_ p . i,c ) & ( a <_ p . i,c implies a <_ o,c ) & ( c <_ o,a implies c <_ p . i,a ) & ( c <_ p . i,a implies c <_ o,a ) ) by A102, A103, Th10;
take o ; :: thesis:
thus S₂[i,o] by A102, A109, A112, A113; :: thesis:

end;

suppose for d being Element of A st d <> b holds
d <_ pII . i,b ; :: thesis:

then a <_ pII . i,b by A102;
then A116: not b <_ pII . i,a by Th4;
consider o being Element of LinPreorders A such that
A117: ( a <_ o,b & c <_ o,b & ( a <_ o,c implies a <_ p . i,c ) & ( a <_ p . i,c implies a <_ o,c ) & ( c <_ o,a implies c <_ p . i,a ) & ( c <_ p . i,a implies c <_ o,a ) ) by A102, A103, Th11;
take o ; :: thesis:
thus S₂[i,o] by A102, A109, A116, A117; :: thesis:

end;

end;

end;

end;

end;

consider pIII being Function of N,(LinPreorders A) such that
A118: for i being Element of N holds S₂[i,pIII . i] from FUNCT_2:sch 3(A106);
reconsider pIII = pIII as Element of Funcs (N,(LinPreorders A)) by FUNCT_2:11;
for i being Element of N holds
( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) )

let i be Element of N; :: thesis:

suppose i = nb ; :: thesis:

then ( a <_ pII . i,b & a <_ pIII . i,b ) by A100, A102, A118;
hence ( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) ) by Th4; :: thesis:

end;

suppose A122: i <> nb ; :: thesis:

per cases by A98;

suppose for d being Element of A st d <> b holds
b <_ pII . i,d ; :: thesis:

then ( b <_ pII . i,a & b <_ pIII . i,a ) by A102, A118, A122;
hence ( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) ) by Th4; :: thesis:

end;

suppose for d being Element of A st d <> b holds
d <_ pII . i,b ; :: thesis:

then ( a <_ pII . i,b & a <_ pIII . i,b ) by A102, A118, A122;
hence ( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) ) by Th4; :: thesis:

end;

end;

end;

end;

end;

then A127: ( a <_ f . pII,b iff a <_ f . pIII,b ) by A2;
for i being Element of N holds
( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) )

let i be Element of N; :: thesis:

suppose i = nb ; :: thesis:

then ( b <_ pI . i,c & b <_ pIII . i,c ) by A99, A103, A118;
hence ( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) ) by Th4; :: thesis:

end;

suppose A131: i <> nb ; :: thesis:

per cases by A98;

suppose A132: for d being Element of A st d <> b holds
b <_ pII . i,d ; :: thesis:

then b <_ pII . i,c by A103;
then A134: b <_ pI . i,c by A96, A131;
b <_ pIII . i,c by A118, A131, A132;
hence ( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) ) by A134, Th4; :: thesis:

end;

suppose A136: for d being Element of A st d <> b holds
d <_ pII . i,b ; :: thesis:

then c <_ pII . i,b by A103;
then A138: c <_ pI . i,b by A96, A131;
c <_ pIII . i,b by A118, A131, A136;
hence ( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) ) by A138, Th4; :: thesis:

end;

end;

end;

end;

end;

then ( b <_ f . pI,c iff b <_ f . pIII,c ) by A2;
then a <_ f . pIII,c by A101, A102, A127, Th5;
hence a <_ f . p,c by A2, A118; :: thesis:

end;

consider b being Element of A;
consider nb being Element of N, pI, pII being Element of Funcs (N,(LinPreorders A)) such that
A142: for i being Element of N st i <> nb holds
pI . i = pII . i and
A143: for i being Element of N holds S₁[pI . i,b] and
A144: ( ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) ) and
A145: for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c by A95;
take nb ; :: thesis:
let p be Element of Funcs (N,(LinPreorders A)); :: thesis:
let a, a9 be Element of A; :: thesis:
assume A146: a <_ p . nb,a9 ; :: thesis:
then A147: a <> a9 by Th4;

suppose ( a <> b & a9 <> b ) ; :: thesis:

hence a <_ f . p,a9 by A145, A146; :: thesis:

end;

suppose A149: ( a = b or a9 = b ) ; :: thesis:

consider c being Element of A such that
A150: ( c <> a & c <> a9 ) by A3, Th2;
consider nc being Element of N, pI9, pII9 being Element of Funcs (N,(LinPreorders A)) such that
for i being Element of N st i <> nc holds
pI9 . i = pII9 . i and
for i being Element of N holds S₁[pI9 . i,c] and
for a being Element of A st a <> c holds
c <_ f . pI9,a and
for a being Element of A st a <> c holds
a <_ f . pII9,c and
A151: for p being Element of Funcs (N,(LinPreorders A))
for a, a9 being Element of A st a <> c & a9 <> c & a <_ p . nc,a9 holds
a <_ f . p,a9 by A95;
nc = nb

per cases by A149;

suppose A153: a = b ; :: thesis:

assume A154: nc <> nb ; :: thesis:
( b <_ pI . nc,a9 or a9 <_ pI . nc,b ) by A143, A147, A153;
then ( ( b <_ pII . nc,a9 & a9 <_ f . pII,b ) or ( a9 <_ pI . nc,b & b <_ f . pI,a9 ) ) by A142, A144, A147, A153, A154;
then ( ( b <_ pII . nc,a9 & a9 <=_ f . pII,b ) or ( a9 <_ pI . nc,b & b <=_ f . pI,a9 ) ) by Th4;
hence contradiction by A150, A151, A153; :: thesis:

end;

suppose A158: a9 = b ; :: thesis:

assume A159: nc <> nb ; :: thesis:
( b <_ pI . nc,a or a <_ pI . nc,b ) by A143, A147, A158;
then ( ( b <_ pII . nc,a & a <_ f . pII,b ) or ( a <_ pI . nc,b & b <_ f . pI,a ) ) by A142, A144, A147, A158, A159;
then ( ( b <_ pII . nc,a & a <=_ f . pII,b ) or ( a <_ pI . nc,b & b <=_ f . pI,a ) ) by Th4;
hence contradiction by A150, A151, A158; :: thesis:

end;

end;

end;

hence a <_ f . p,a9 by A146, A150, A151; :: thesis:

end;

end;