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

suppose A10: 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 A8, A9, A10; :: thesis:

end;

suppose A11: a9 = c9 ; :: thesis:

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

per cases by Th4;

suppose A13: 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 A9, A11, A12, A13; :: thesis:

end;

suppose A14: 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 A8, A12, A14; :: thesis:

end;

end;

end;

end;

end;

then consider a, c being Element of A such that
A15: ( a <> b & b <> c ) and
A16: a <> c and
A17: ( 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 );
A18: 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 A7;

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

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

end;

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

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

end;

end;

end;

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

end;

A24: 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
A25: rng t = N and
A26: t is one-to-one by FINSEQ_4:58;
reconsider t = t as FinSequence of N by A25, FINSEQ_1:def 4;
let b be Element of A; :: thesis:
consider oI being Element of LinPreorders A such that
A27: for a being Element of A st a <> b holds
b <_ oI,a by Th8;
consider oII being Element of LinPreorders A such that
A28: for a being Element of A st a <> b holds
a <_ oII,b by Th9;
A29: 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 ) );
A30: 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 object such that
A31: k in dom t and
A32: i = t . k by A25, FUNCT_1:def 3;
reconsider k = k as Nat by A31;

suppose A33: k < k0 ; :: thesis:

take oII ; :: thesis:
thus S₂[i,oII] by A31, A32, A33; :: thesis:

end;

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

take oI ; :: thesis:
thus S₂[i,oI] by A31, A32, A34; :: thesis:

end;

end;

end;

consider p being Function of N,(LinPreorders A) such that
A35: for i being Element of N holds S₂[i,p . i] from FUNCT_2:sch 3(A30);
reconsider p = p as Element of Funcs (N,(LinPreorders A)) by FUNCT_2:8;
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
A36: k in dom t and
A37: k < k0 ; :: thesis:
reconsider i = t . k as Element of N by A36, PARTFUN1:4;
S₂[i,p . i] by A35;
hence p . (t . k) = oII by A26, A36, A37, FUNCT_1:def 4; :: thesis:

end;

let k be Nat; :: thesis:
assume that
A38: k in dom t and
A39: k >= k0 ; :: thesis:
reconsider i = t . k as Element of N by A38, PARTFUN1:4;
S₂[i,p . i] by A35;
hence p . (t . k) = oI by A26, A38, A39, FUNCT_1:def 4; :: 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 12;
A40: S₂[kII9]

let p be Element of Funcs (N,(LinPreorders A)); :: thesis:
assume that
A41: 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 A42: a <> b ; :: thesis:
for i being Element of N holds a <_ p . i,b

let i be Element of N; :: thesis:
consider k being object such that
A43: k in dom t and
A44: i = t . k by A25, FUNCT_1:def 3;
reconsider k = k as Nat by A43;
k <= len t by A43, FINSEQ_3:25;
then k + 0 < kII9 by XREAL_1:8;
then p . i = oII by A41, A43, A44;
hence a <_ p . i,b by A28, A42; :: thesis:

end;

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

end;

then A45: ex kII9 being Nat st S₂[kII9] ;
consider kII being Nat such that
A46: ( S₂[kII] & ( for k0 being Nat st S₂[k0] holds
k0 >= kII ) ) from NAT_1:sch 5(A45);
consider pII being Element of Funcs (N,(LinPreorders A)) such that
A47: for k being Nat st k in dom t & k < kII holds
pII . (t . k) = oII and
A48: for k being Nat st k in dom t & k >= kII holds
pII . (t . k) = oI by A29;
A49: kII > 1

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

let i be Element of N; :: thesis:
consider k being object such that
A53: k in dom t and
A54: i = t . k by A25, FUNCT_1:def 3;
reconsider k = k as Nat by A53;
k >= 1 by A53, FINSEQ_3:25;
then pII . i = oI by A48, A50, A53, A54, XXREAL_0:2;
hence b <_ pII . i,a by A27, A51; :: thesis:

end;

A55: a <_ f . pII,b by A46, A47, A48, A51;
b <_ f . pII,a by A1, A52;
hence contradiction by A55, Th4; :: thesis:

end;

then reconsider kI = kII - 1 as Nat by NAT_1:20;
reconsider kI = kI as Element of NAT by ORDINAL1:def 12;
A56: kII = kI + 1 ;
kI > 1 - 1 by A49, XREAL_1:9;
then A57: kI >= 0 + 1 by INT_1:7;
kII <= kII9 by A40, A46;
then kI <= kII9 - 1 by XREAL_1:9;
then A58: kI in dom t by A57, FINSEQ_3:25;
then reconsider nb = t . kI as Element of N by PARTFUN1:4;
A59: kI + 0 < kII by A56, XREAL_1:8;
then consider pI being Element of Funcs (N,(LinPreorders A)) such that
A60: for k being Nat st k in dom t & k < kI holds
pI . (t . k) = oII and
A61: for k being Nat st k in dom t & k >= kI holds
pI . (t . k) = oI and
A62: ex a being Element of A st
( a <> b & not a <_ f . pI,b ) by A46;
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 A63: i <> nb ; :: thesis:
consider k being object such that
A64: k in dom t and
A65: i = t . k by A25, FUNCT_1:def 3;
reconsider k = k as Nat by A64;

per cases by A63, A65, XXREAL_0:1;

suppose k < kI ; :: thesis:

then ( k + 0 < kII & pI . i = oII ) by A56, A60, A64, A65, XREAL_1:8;
hence pI . i = pII . i by A47, A64, A65; :: thesis:

end;

suppose k > kI ; :: thesis:

then ( k >= kII & pI . i = oI ) by A56, A61, A64, A65, INT_1:7;
hence pI . i = pII . i by A48, A64, A65; :: thesis:

end;

end;

end;

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

let i be Element of N; :: thesis:
ex k being object st
( k in dom t & i = t . k ) by A25, FUNCT_1:def 3;
then ( pI . i = oII or pI . i = oI ) by A60, A61;
hence S₁[pI . i,b] by A27, A28; :: 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 object st
( k in dom t & i = t . k ) by A25, FUNCT_1:def 3;
then ( pII . i = oII or pII . i = oI ) by A47, A48;
hence S₁[pII . i,b] by A27, A28; :: thesis:

end;

pI . nb = oI by A58, A61;
hence for a being Element of A st a <> b holds
b <_ pI . nb,a by A27; :: thesis:
pII . nb = oII by A47, A58, A59;
hence for a being Element of A st a <> b holds
a <_ pII . nb,b by A28; :: thesis:
thus for a being Element of A st a <> b holds
b <_ f . pI,a by A4, A62, A66; :: thesis:
thus for a being Element of A st a <> b holds
a <_ f . pII,b by A46, A47, A48; :: thesis:

end;

A67: 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
A68: for i being Element of N st i <> nb holds
pI . i = pII . i and
A69: for i being Element of N holds S₁[pI . i,b] and
A70: for i being Element of N holds S₁[pII . i,b] and
A71: for a being Element of A st a <> b holds
b <_ pI . nb,a and
A72: for a being Element of A st a <> b holds
a <_ pII . nb,b and
A73: ( ( 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 A24;
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 A68, A69, A73; :: thesis:
let p be Element of Funcs (N,(LinPreorders A)); :: thesis:
let a, c be Element of A; :: thesis:
assume that
A74: a <> b and
A75: c <> b and
A76: a <_ p . nb,c ; :: thesis:
A77: a <> c by A76, 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 ) ) ) ) );
A78: 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 A79: i = nb ; :: thesis:

consider o being Element of LinPreorders A such that
A80: ( a <_ o,b & b <_ o,c ) by A74, A75, A77, Th7;
take o ; :: thesis:
thus S₂[i,o] by A76, A79, A80, Th4, Th5; :: thesis:

end;

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

per cases by A70;

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

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

end;

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

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

end;

end;

end;

end;

end;

consider pIII being Function of N,(LinPreorders A) such that
A86: for i being Element of N holds S₂[i,pIII . i] from FUNCT_2:sch 3(A78);
reconsider pIII = pIII as Element of Funcs (N,(LinPreorders A)) by FUNCT_2:8;
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 A72, A74, A86;
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 A87: i <> nb ; :: thesis:

per cases by A70;

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 A74, A86, A87;
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 A74, A86, A87;
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 A88: ( 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 A71, A75, A86;
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 A89: i <> nb ; :: thesis:

per cases by A70;

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

then b <_ pII . i,c by A75;
then A91: b <_ pI . i,c by A68, A89;
b <_ pIII . i,c by A86, A89, A90;
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 A91, Th4; :: thesis:

end;

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

then c <_ pII . i,b by A75;
then A93: c <_ pI . i,b by A68, A89;
c <_ pIII . i,b by A86, A89, A92;
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 A93, 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 A73, A74, A88, Th5;
hence a <_ f . p,c by A2, A86; :: thesis:

end;

set b = the Element of A;
consider nb being Element of N, pI, pII being Element of Funcs (N,(LinPreorders A)) such that
A94: for i being Element of N st i <> nb holds
pI . i = pII . i and
A95: for i being Element of N holds S₁[pI . i, the Element of A] and
A96: ( ( for a being Element of A st a <> the Element of A holds
the Element of A <_ f . pI,a ) & ( for a being Element of A st a <> the Element of A holds
a <_ f . pII, the Element of A ) ) and
A97: for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> the Element of A & c <> the Element of A & a <_ p . nb,c holds
a <_ f . p,c by A67;
take nb ; :: thesis:
let p be Element of Funcs (N,(LinPreorders A)); :: thesis:
let a, a9 be Element of A; :: thesis:
assume A98: a <_ p . nb,a9 ; :: thesis:
then A99: a <> a9 by Th4;

suppose ( a <> the Element of A & a9 <> the Element of A ) ; :: thesis:

hence a <_ f . p,a9 by A97, A98; :: thesis:

end;

suppose A100: ( a = the Element of A or a9 = the Element of A ) ; :: thesis:

consider c being Element of A such that
A101: ( 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
A102: 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 A67;
nc = nb

per cases by A100;

suppose A103: a = the Element of A ; :: thesis:

assume A104: nc <> nb ; :: thesis:
( the Element of A <_ pI . nc,a9 or a9 <_ pI . nc, the Element of A ) by A95, A99, A103;
then ( ( the Element of A <_ pII . nc,a9 & a9 <_ f . pII, the Element of A ) or ( a9 <_ pI . nc, the Element of A & the Element of A <_ f . pI,a9 ) ) by A94, A96, A99, A103, A104;
then ( ( the Element of A <_ pII . nc,a9 & a9 <=_ f . pII, the Element of A ) or ( a9 <_ pI . nc, the Element of A & the Element of A <=_ f . pI,a9 ) ) by Th4;
hence contradiction by A101, A102, A103; :: thesis:

end;

suppose A105: a9 = the Element of A ; :: thesis:

assume A106: nc <> nb ; :: thesis:
( the Element of A <_ pI . nc,a or a <_ pI . nc, the Element of A ) by A95, A99, A105;
then ( ( the Element of A <_ pII . nc,a & a <_ f . pII, the Element of A ) or ( a <_ pI . nc, the Element of A & the Element of A <_ f . pI,a ) ) by A94, A96, A99, A105, A106;
then ( ( the Element of A <_ pII . nc,a & a <=_ f . pII, the Element of A ) or ( a <_ pI . nc, the Element of A & the Element of A <=_ f . pI,a ) ) by Th4;
hence contradiction by A101, A102, A105; :: thesis:

end;

end;

end;

hence a <_ f . p,a9 by A98, A101, A102; :: thesis:

end;

end;