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, 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 implies a <_ p' . i,b ) & ( a <_ p' . i,b implies a <_ p . i,b ) & ( b <_ p . i,a implies b <_ p' . i,a ) & ( b <_ p' . i,a implies b <_ p . i,a ) ) ) holds
( a <_ f . p,b iff a <_ f . p',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]

proof

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
A5: ( ex a being Element of A st
( a <> b & a <=_ f . p,b ) & ex c being Element of A st
( c <> b & b <=_ f . p,c ) & ( for i being Element of N holds S₁[p . i,b] ) ) ;
consider a' being Element of A such that
A6: ( a' <> b & a' <=_ f . p,b ) by A5;
consider c' being Element of A such that
A7: ( b <> c' & b <=_ f . p,c' ) by A5;
ex a, c being Element of A st
( a <> b & b <> c & a <> c & a <=_ f . p,b & b <=_ f . p,c )

proof

per cases ;

suppose A8: a' <> c' ; :: thesis:

take a' ; :: thesis:
take c' ; :: thesis:
thus ( a' <> b & b <> c' & a' <> c' & a' <=_ f . p,b & b <=_ f . p,c' ) by A6, A7, A8; :: thesis:

end;

suppose A9: a' = c' ; :: thesis:

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

per cases by Th4;

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

take d ; :: thesis:
take c' ; :: thesis:
thus ( d <> b & b <> c' & d <> c' & d <=_ f . p,b & b <=_ f . p,c' ) by A7, A9, A10, A11; :: thesis:

end;

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

take a' ; :: thesis:
take d ; :: thesis:
thus ( a' <> b & b <> d & a' <> d & a' <=_ f . p,b & b <=_ f . p,d ) by A6, A10, A12; :: thesis:

end;

then consider a, c being Element of A such that
A13: ( a <> b & b <> c & a <> c & 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 );
A14: for i being Element of N ex o being Element of LinPreorders A st S₂[i,o]

proof

let i be Element of N; :: thesis:

per cases by A5;

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

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

end;

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

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

end;

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

end;

A20: 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 ) )

proof

consider t being FinSequence such that
A21: ( rng t = N & t is one-to-one ) by FINSEQ_4:73;
reconsider t = t as FinSequence of N by A21, FINSEQ_1:def 4;
let b be Element of A; :: thesis:
consider oI being Element of LinPreorders A such that
A22: for a being Element of A st a <> b holds
b <_ oI,a by Th8;
consider oII being Element of LinPreorders A such that
A23: for a being Element of A st a <> b holds
a <_ oII,b by Th9;
A24: 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 ) )

proof

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 ) );
A25: for i being Element of N ex o being Element of LinPreorders A st S₂[i,o]

proof

let i be Element of N; :: thesis:
consider k being set such that
A26: ( k in dom t & i = t . k ) by A21, FUNCT_1:def 5;
reconsider k = k as Nat by A26;

per cases ;

suppose A27: k < k0 ; :: thesis:

take oII ; :: thesis:
thus S₂[i,oII] by A26, A27; :: thesis:

end;

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

take oI ; :: thesis:
thus S₂[i,oI] by A26, A28; :: thesis:

end;

consider p being Function of N,(LinPreorders A) such that
A29: for i being Element of N holds S₂[i,p . i] from FUNCT_2:sch 3(A25);
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:

proof

let k be Nat; :: thesis:
assume A30: ( k in dom t & k < k0 ) ; :: thesis:
then reconsider i = t . k as Element of N by PARTFUN1:27;
S₂[i,p . i] by A29;
hence p . (t . k) = oII by A21, A30, FUNCT_1:def 8; :: thesis:

end;

let k be Nat; :: thesis:
assume A31: ( k in dom t & k >= k0 ) ; :: thesis:
then reconsider i = t . k as Element of N by PARTFUN1:27;
S₂[i,p . i] by A29;
hence p . (t . k) = oI by A21, A31, 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 kII' = (len t) + 1 as Element of NAT by ORDINAL1:def 13;
A32: S₂[kII']

proof

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

proof

let i be Element of N; :: thesis:
consider k being set such that
A35: ( k in dom t & i = t . k ) by A21, FUNCT_1:def 5;
reconsider k = k as Nat by A35;
k <= len t by A35, FINSEQ_3:27;
then k + 0 < kII' by XREAL_1:10;
then p . i = oII by A33, A35;
hence a <_ p . i,b by A23, A34; :: thesis:

end;

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

end;

then A36: ex kII' being Nat st S₂[kII'] ;
consider kII being Nat such that
A37: ( S₂[kII] & ( for k0 being Nat st S₂[k0] holds
k0 >= kII ) ) from NAT_1:sch 5(A36);
consider pII being Element of Funcs N,(LinPreorders A) such that
A38: ( ( for k being Nat st k in dom t & k < kII holds
pII . (t . k) = oII ) & ( for k being Nat st k in dom t & k >= kII holds
pII . (t . k) = oI ) ) by A24;
A39: kII > 1

proof

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

proof

let i be Element of N; :: thesis:
consider k being set such that
A42: ( k in dom t & i = t . k ) by A21, FUNCT_1:def 5;
reconsider k = k as Nat by A42;
k >= 1 by A42, FINSEQ_3:27;
then k >= kII by A40, XXREAL_0:2;
then pII . i = oI by A38, A42;
hence b <_ pII . i,a by A22, A41; :: thesis:

end;

then ( a <_ f . pII,b & b <_ f . pII,a ) by A1, A37, A38, A41;
hence contradiction by 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;
A43: kII = kI + 1 ;
kI > 1 - 1 by A39, XREAL_1:11;
then A44: kI >= 0 + 1 by INT_1:20;
kII <= kII' by A32, A37;
then kI <= kII' - 1 by XREAL_1:11;
then A45: kI in dom t by A44, FINSEQ_3:27;
then reconsider nb = t . kI as Element of N by PARTFUN1:27;
A46: kI + 0 < kII by A43, XREAL_1:10;
then consider pI being Element of Funcs N,(LinPreorders A) such that
A47: ( ( for k being Nat st k in dom t & k < kI holds
pI . (t . k) = oII ) & ( for k being Nat st k in dom t & k >= kI holds
pI . (t . k) = oI ) & ex a being Element of A st
( a <> b & not a <_ f . pI,b ) ) by A37;
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:

proof

let i be Element of N; :: thesis:
assume A48: i <> nb ; :: thesis:
consider k being set such that
A49: ( k in dom t & i = t . k ) by A21, FUNCT_1:def 5;
reconsider k = k as Nat by A49;

per cases by A48, A49, XXREAL_0:1;

suppose k < kI ; :: thesis:

then ( k < kI & k + 0 < kII ) by A43, XREAL_1:10;
then ( pI . i = oII & pII . i = oII ) by A38, A47, A49;
hence pI . i = pII . i ; :: thesis:

end;

suppose k > kI ; :: thesis:

then ( k >= kI & k >= kII ) by A43, INT_1:20;
then ( pI . i = oI & pII . i = oI ) by A38, A47, A49;
hence pI . i = pII . i ; :: thesis:

end;

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

proof

let i be Element of N; :: thesis:
consider k being set such that
A51: ( k in dom t & i = t . k ) by A21, FUNCT_1:def 5;
( pI . i = oII or pI . i = oI ) by A47, A51;
hence S₁[pI . i,b] by A22, A23; :: thesis:

end;

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

proof

let i be Element of N; :: thesis:
consider k being set such that
A52: ( k in dom t & i = t . k ) by A21, FUNCT_1:def 5;
( pII . i = oII or pII . i = oI ) by A38, A52;
hence S₁[pII . i,b] by A22, A23; :: thesis:

end;

pI . nb = oI by A45, A47;
hence for a being Element of A st a <> b holds
b <_ pI . nb,a by A22; :: thesis:
pII . nb = oII by A38, A45, A46;
hence for a being Element of A st a <> b holds
a <_ pII . nb,b by A23; :: thesis:
thus for a being Element of A st a <> b holds
b <_ f . pI,a by A4, A47, A50; :: thesis:
thus for a being Element of A st a <> b holds
a <_ f . pII,b by A37, A38; :: thesis:

end;

A53: 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 ) )

proof

let b be Element of A; :: thesis:
consider nb being Element of N, pI, pII being Element of Funcs N,(LinPreorders A) such that
A54: for i being Element of N st i <> nb holds
pI . i = pII . i and
A55: for i being Element of N holds S₁[pI . i,b] and
A56: for i being Element of N holds S₁[pII . i,b] and
A57: for a being Element of A st a <> b holds
b <_ pI . nb,a and
A58: for a being Element of A st a <> b holds
a <_ pII . nb,b and
A59: for a being Element of A st a <> b holds
b <_ f . pI,a and
A60: for a being Element of A st a <> b holds
a <_ f . pII,b by A20;
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 A54, A55, A59, A60; :: thesis:
let p be Element of Funcs N,(LinPreorders A); :: thesis:
let a, c be Element of A; :: thesis:
assume that
A61: ( a <> b & c <> b ) and
A62: a <_ p . nb,c ; :: thesis:
A63: a <> c by A62, 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 ) ) ) ) );
A64: for i being Element of N ex o being Element of LinPreorders A st S₂[i,o]

proof

let i be Element of N; :: thesis:

per cases ;

suppose A65: i = nb ; :: thesis:

consider o being Element of LinPreorders A such that
A66: ( a <_ o,b & b <_ o,c ) by A61, A63, Th7;
take o ; :: thesis:
thus S₂[i,o] by A62, A65, A66, Th4, Th5; :: thesis:

end;

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

per cases by A56;

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

then b <_ pII . i,a by A61;
then A68: not a <_ pII . i,b by Th4;
consider o being Element of LinPreorders A such that
A69: ( 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 A61, Th10;
take o ; :: thesis:
thus S₂[i,o] by A61, A67, A68, A69; :: thesis:

end;

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

then a <_ pII . i,b by A61;
then A70: not b <_ pII . i,a by Th4;
consider o being Element of LinPreorders A such that
A71: ( 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 A61, Th11;
take o ; :: thesis:
thus S₂[i,o] by A61, A67, A70, A71; :: thesis:

end;

consider pIII being Function of N,(LinPreorders A) such that
A72: for i being Element of N holds S₂[i,pIII . i] from FUNCT_2:sch 3(A64);
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 ) )

proof

let i be Element of N; :: thesis:

per cases ;

suppose i = nb ; :: thesis:

then ( a <_ pII . i,b & a <_ pIII . i,b ) by A58, A61, A72;
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 A73: i <> nb ; :: thesis:

per cases by A56;

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 A61, A72, A73;
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 A61, A72, A73;
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;

then A74: ( 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 ) )

proof

let i be Element of N; :: thesis:

per cases ;

suppose i = nb ; :: thesis:

then ( b <_ pI . i,c & b <_ pIII . i,c ) by A57, A61, A72;
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 A75: i <> nb ; :: thesis:

per cases by A56;

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

then ( b <_ pII . i,c & b <_ pIII . i,c ) by A61, A72, A75;
then ( b <_ pI . i,c & b <_ pIII . i,c ) by A54, A75;
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 for d being Element of A st d <> b holds
d <_ pII . i,b ; :: thesis:

then ( c <_ pII . i,b & c <_ pIII . i,b ) by A61, A72, A75;
then ( c <_ pI . i,b & c <_ pIII . i,b ) by A54, A75;
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;

then ( b <_ f . pI,c iff b <_ f . pIII,c ) by A2;
then a <_ f . pIII,c by A59, A60, A61, A74, Th5;
hence a <_ f . p,c by A2, A72; :: 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
A76: for i being Element of N st i <> nb holds
pI . i = pII . i and
A77: for i being Element of N holds S₁[pI . i,b] and
A78: for a being Element of A st a <> b holds
b <_ f . pI,a and
A79: for a being Element of A st a <> b holds
a <_ f . pII,b and
A80: 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 A53;
take nb ; :: thesis:
let p be Element of Funcs N,(LinPreorders A); :: thesis:
let a, a' be Element of A; :: thesis:
assume A81: a <_ p . nb,a' ; :: thesis:
then A82: a <> a' by Th4;

per cases ;

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

hence a <_ f . p,a' by A80, A81; :: thesis:

end;

suppose A83: ( a = b or a' = b ) ; :: thesis:

consider c being Element of A such that
A84: ( c <> a & c <> a' ) by A3, Th2;
consider nc being Element of N, pI', pII' being Element of Funcs N,(LinPreorders A) such that
for i being Element of N st i <> nc holds
pI' . i = pII' . i and
for i being Element of N holds S₁[pI' . i,c] and
for a being Element of A st a <> c holds
c <_ f . pI',a and
for a being Element of A st a <> c holds
a <_ f . pII',c and
A85: for p being Element of Funcs N,(LinPreorders A)
for a, a' being Element of A st a <> c & a' <> c & a <_ p . nc,a' holds
a <_ f . p,a' by A53;
nc = nb

proof

per cases by A83;

suppose A86: a = b ; :: thesis:

assume A87: nc <> nb ; :: thesis:
( b <_ pI . nc,a' or a' <_ pI . nc,b ) by A77, A82, A86;
then ( ( b <_ pII . nc,a' & a' <_ f . pII,b ) or ( a' <_ pI . nc,b & b <_ f . pI,a' ) ) by A76, A78, A79, A82, A86, A87;
then ( ( b <_ pII . nc,a' & a' <=_ f . pII,b ) or ( a' <_ pI . nc,b & b <=_ f . pI,a' ) ) by Th4;
hence contradiction by A84, A85, A86; :: thesis:

end;

suppose A88: a' = b ; :: thesis:

assume A89: nc <> nb ; :: thesis:
( b <_ pI . nc,a or a <_ pI . nc,b ) by A77, A82, A88;
then ( ( b <_ pII . nc,a & a <_ f . pII,b ) or ( a <_ pI . nc,b & b <_ f . pI,a ) ) by A76, A78, A79, A82, A88, A89;
then ( ( b <_ pII . nc,a & a <=_ f . pII,b ) or ( a <_ pI . nc,b & b <=_ f . pI,a ) ) by Th4;
hence contradiction by A84, A85, A88; :: thesis:

end;

hence a <_ f . p,a' by A81, A84, A85; :: thesis:

end;