:: ARROW semantic presentation

begin

definition
let A, B9 be non empty set ;
let B be non empty Subset of B9;
let f be Function of A,B;
let x be Element of A;
:: original: .
redefine funcf . x ->  Element of B;
coherence
 f . x is Element of B
proof
thus  f . x is Element of B ; ::_thesis: verum
end;
end;

theorem Th1: :: ARROW:1
for A being finite set st card A >= 2 holds
for a being Element of A ex b being Element of A st b <> a
proof
let A9 be finite set ; ::_thesis: ( card A9 >= 2 implies for a being Element of A9 ex b being Element of A9 st b <> a )
assume A1: card A9 >= 2 ; ::_thesis: for a being Element of A9 ex b being Element of A9 st b <> a
then reconsider A = A9 as non empty finite set by CARD_1:27;
let a be Element of A9; ::_thesis: ex b being Element of A9 st b <> a
 {a} c= A by ZFMISC_1:31;
then  card (A \ {a}) = (card A) - (card {a}) by CARD_2:44
.= (card A) - 1 by CARD_1:30 ;
then  card (A \ {a}) <> 0 by A1;
then consider b being set  such that
A2: b in A \ {a} by CARD_1:27, XBOOLE_0:def_1;
reconsider b = b as Element of A9 by A2;
take  b ; ::_thesis: b <> a
 not b in {a} by A2, XBOOLE_0:def_5;
hence  b <> a by TARSKI:def_1; ::_thesis: verum
end;

theorem Th2: :: ARROW:2
for A being finite set st card A >= 3 holds
for a, b being Element of A ex c being Element of A st
( c <> a & c <> b )
proof
let A9 be finite set ; ::_thesis: ( card A9 >= 3 implies for a, b being Element of A9 ex c being Element of A9 st
( c <> a & c <> b ) )
assume A1: card A9 >= 3 ; ::_thesis: for a, b being Element of A9 ex c being Element of A9 st
( c <> a & c <> b )
then reconsider A = A9 as non empty finite set by CARD_1:27;
let a, b be Element of A9; ::_thesis: ex c being Element of A9 st
( c <> a & c <> b )
 {a,b} c= A by ZFMISC_1:32;
then A2: card (A \ {a,b}) = (card A) - (card {a,b}) by CARD_2:44;
 card {a,b} <= 2 by CARD_2:50;
then  card (A \ {a,b}) >= 3 - 2 by A1, A2, XREAL_1:13;
then  card (A \ {a,b}) <> 0 ;
then consider c being set  such that
A3: c in A \ {a,b} by CARD_1:27, XBOOLE_0:def_1;
reconsider c = c as Element of A9 by A3;
take  c ; ::_thesis: ( c <> a & c <> b )
 not c in {a,b} by A3, XBOOLE_0:def_5;
hence  ( c <> a & c <> b ) by TARSKI:def_2; ::_thesis: verum
end;

begin


definition
let A be non empty set ;
defpred S1[ set ] means ( $1 is Relation of A & ( for a, b being Element of A holds
( [a,b] in $1 or [b,a] in $1 ) ) & ( for a, b, c being Element of A st [a,b] in $1 & [b,c] in $1 holds
[a,c] in $1 ) );
defpred S2[ set ] means  for R being set holds
( R in $1 iff S1[R] );
func LinPreorders A ->  set  means :Def1: :: ARROW:def 1
 for R being set holds
( R in it iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) );
existence
 ex b1 being set st
for R being set holds
( R in b1 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) )
proof
consider it0 being set  such that
A1: for R being set holds
( R in it0 iff ( R in bool [:A,A:] & S1[R] ) ) from XBOOLE_0:sch_1();
take  it0 ; ::_thesis: for R being set holds
( R in it0 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) )
let R be set ; ::_thesis: ( R in it0 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) )
thus  ( R in it0 implies S1[R] ) by A1; ::_thesis: ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) implies R in it0 )
assume A2: S1[R] ; ::_thesis: R in it0
 [:A,A:] in bool [:A,A:] by ZFMISC_1:def_1;
hence  R in it0 by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for R being set holds
( R in b1 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) ) & ( for R being set holds
( R in b2 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) ) holds
b1 = b2
proof
let it1, it2 be set ; ::_thesis: ( ( for R being set holds
( R in it1 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) ) & ( for R being set holds
( R in it2 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) ) implies it1 = it2 )
assume that
A3: S2[it1] and
A4: S2[it2] ; ::_thesis: it1 = it2
now__::_thesis:_for_R_being_set_holds_
(_R_in_it1_iff_R_in_it2_)
let R be set ; ::_thesis: ( R in it1 iff R in it2 )
 ( R in it1 iff S1[R] ) by A3;
hence  ( R in it1 iff R in it2 ) by A4; ::_thesis: verum
end;
hence  it1 = it2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines LinPreorders ARROW:def_1_:_
 for A being non empty set
for b2 being set holds
( b2 = LinPreorders A iff for R being set holds
( R in b2 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) );

registration
let A be non empty set ;
cluster LinPreorders A ->  non empty ;
coherence
 not LinPreorders A is empty
proof
 [:A,A:] c= [:A,A:] ;
then reconsider R = [:A,A:] as Relation of A ;
 ( ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) by ZFMISC_1:87;
hence  not LinPreorders A is empty by Def1; ::_thesis: verum
end;
end;

definition
let A be non empty set ;
defpred S1[ set ] means  for a, b being Element of A st [a,b] in $1 & [b,a] in $1 holds
a = b;
defpred S2[ set ] means  for R being Element of LinPreorders A holds
( R in $1 iff S1[R] );
func LinOrders A ->  Subset of (LinPreorders A) means :Def2: :: ARROW:def 2
 for R being Element of LinPreorders A holds
( R in it iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b );
existence
 ex b1 being Subset of (LinPreorders A) st
for R being Element of LinPreorders A holds
( R in b1 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b )
proof
consider it0 being set  such that
A1: for R being set holds
( R in it0 iff ( R in LinPreorders A & S1[R] ) ) from XBOOLE_0:sch_1();
 for R being set st R in it0 holds
R in LinPreorders A by A1;
then reconsider it0 = it0 as Subset of (LinPreorders A) by TARSKI:def_3;
take  it0 ; ::_thesis: for R being Element of LinPreorders A holds
( R in it0 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b )
let R be Element of LinPreorders A; ::_thesis: ( R in it0 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b )
thus  ( R in it0 implies S1[R] ) by A1; ::_thesis: ( ( for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) implies R in it0 )
assume  S1[R] ; ::_thesis: R in it0
hence  R in it0 by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (LinPreorders A) st ( for R being Element of LinPreorders A holds
( R in b1 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) & ( for R being Element of LinPreorders A holds
( R in b2 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) holds
b1 = b2
proof
let it1, it2 be Subset of (LinPreorders A); ::_thesis: ( ( for R being Element of LinPreorders A holds
( R in it1 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) & ( for R being Element of LinPreorders A holds
( R in it2 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) implies it1 = it2 )
assume that
A2: S2[it1] and
A3: S2[it2] ; ::_thesis: it1 = it2
now__::_thesis:_for_R_being_Element_of_LinPreorders_A_holds_
(_R_in_it1_iff_R_in_it2_)
let R be Element of LinPreorders A; ::_thesis: ( R in it1 iff R in it2 )
 ( R in it1 iff S1[R] ) by A2;
hence  ( R in it1 iff R in it2 ) by A3; ::_thesis: verum
end;
hence  it1 = it2 by SUBSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines LinOrders ARROW:def_2_:_
 for A being non empty set
for b2 being Subset of (LinPreorders A) holds
( b2 = LinOrders A iff for R being Element of LinPreorders A holds
( R in b2 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) );

registration
let A be set ;
cluster Relation-like A -defined A -valued V17(A) reflexive antisymmetric connected transitive for Element of bool [:A,A:];
existence
 ex b1 being Order of A st b1 is connected
proof
consider R9 being Relation such that
A1: R9 well_orders A by WELLORD2:17;
set R = R9 |_2 A;
A2: R9 |_2 A is well-ordering by A1, WELLORD2:16;
reconsider R = R9 |_2 A as Relation of A by XBOOLE_1:17;
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_dom_R
let a be set ; ::_thesis: ( a in A implies a in dom R )
assume A3: a in A ; ::_thesis: a in dom R
 R9 is_reflexive_in A by A1, WELLORD1:def_5;
then A4: [a,a] in R9 by A3, RELAT_2:def_1;
 [a,a] in [:A,A:] by A3, ZFMISC_1:def_2;
then  [a,a] in R by A4, XBOOLE_0:def_4;
hence  a in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
then  A c= dom R by TARSKI:def_3;
then  dom R = A by XBOOLE_0:def_10;
then reconsider R = R as Order of A by A2, PARTFUN1:def_2, WELLORD1:def_4;
take  R ; ::_thesis: R is connected
thus  R is connected by A2, WELLORD1:def_4; ::_thesis: verum
end;
end;

definition
let A be non empty set ;
redefine func LinOrders A means :Def3: :: ARROW:def 3
 for R being set holds
( R in it iff R is connected Order of A );
compatibility
 for b1 being Subset of (LinPreorders A) holds
( b1 = LinOrders A iff for R being set holds
( R in b1 iff R is connected Order of A ) )
proof
A1: now__::_thesis:_for_R_being_set_st_R_in_LinOrders_A_holds_
R_is_connected_Order_of_A
let R be set ; ::_thesis: ( R in LinOrders A implies R is connected Order of A )
assume A2: R in LinOrders A ; ::_thesis: R is connected Order of A
then reconsider R9 = R as Relation of A by Def1;
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_dom_R9
let a be set ; ::_thesis: ( a in A implies a in dom R9 )
assume  a in A ; ::_thesis: a in dom R9
then  [a,a] in R by A2, Def1;
hence  a in dom R9 by XTUPLE_0:def_12; ::_thesis: verum
end;
then  A c= dom R9 by TARSKI:def_3;
then A3: dom R9 = A by XBOOLE_0:def_10;
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_rng_R9
let a be set ; ::_thesis: ( a in A implies a in rng R9 )
assume  a in A ; ::_thesis: a in rng R9
then  [a,a] in R by A2, Def1;
hence  a in rng R9 by XTUPLE_0:def_13; ::_thesis: verum
end;
then  A c= rng R9 by TARSKI:def_3;
then A4: field R9 = A \/ A by A3, XBOOLE_0:def_10;
 for a, b being set st a in A & b in A & a <> b & not [a,b] in R holds
[b,a] in R by A2, Def1;
then A5: R9 is_connected_in A by RELAT_2:def_6;
 for a being set st a in A holds
[a,a] in R by A2, Def1;
then A6: R9 is_reflexive_in A by RELAT_2:def_1;
 for a, b being set st a in A & b in A & [a,b] in R & [b,a] in R holds
a = b by A2, Def2;
then A7: R9 is_antisymmetric_in A by RELAT_2:def_4;
 for a, b, c being set st a in A & b in A & c in A & [a,b] in R & [b,c] in R holds
[a,c] in R by A2, Def1;
then  R9 is_transitive_in A by RELAT_2:def_8;
hence  R is connected Order of A by A3, A4, A5, A6, A7, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_14, RELAT_2:def_16; ::_thesis: verum
end;
A8: now__::_thesis:_for_R_being_set_st_R_is_connected_Order_of_A_holds_
R_in_LinOrders_A
let R be set ; ::_thesis: ( R is connected Order of A implies R in LinOrders A )
assume A9: R is connected Order of A ; ::_thesis: R in LinOrders A
then reconsider R9 = R as connected Order of A ;
A10: now__::_thesis:_for_a,_b_being_Element_of_A_holds_
(_[a,b]_in_R_or_[b,a]_in_R_)
let a, b be Element of A; ::_thesis: ( [a,b] in R or [b,a] in R )
 dom R9 = A by PARTFUN1:def_2;
then  A c= (dom R9) \/ (rng R9) by XBOOLE_1:7;
then A11: field R9 = A by XBOOLE_0:def_10;
A12: ( R9 is_connected_in field R9 & R9 is_reflexive_in field R9 ) by RELAT_2:def_9, RELAT_2:def_14;
 ( a = b or a <> b ) ;
hence  ( [a,b] in R or [b,a] in R ) by A11, A12, RELAT_2:def_1, RELAT_2:def_6; ::_thesis: verum
end;
 for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R by A9, ORDERS_1:5;
then A13: R in LinPreorders A by A9, A10, Def1;
 for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b by A9, ORDERS_1:4;
hence  R in LinOrders A by A13, Def2; ::_thesis: verum
end;
let it0 be Subset of (LinPreorders A); ::_thesis: ( it0 = LinOrders A iff for R being set holds
( R in it0 iff R is connected Order of A ) )
thus  ( it0 = LinOrders A implies for R being set holds
( R in it0 iff R is connected Order of A ) ) by A1, A8; ::_thesis: ( ( for R being set holds
( R in it0 iff R is connected Order of A ) ) implies it0 = LinOrders A )
assume A14: for R being set holds
( R in it0 iff R is connected Order of A ) ; ::_thesis: it0 = LinOrders A
now__::_thesis:_for_R_being_set_holds_
(_R_in_it0_iff_R_in_LinOrders_A_)
let R be set ; ::_thesis: ( R in it0 iff R in LinOrders A )
 ( R in it0 iff R is connected Order of A ) by A14;
hence  ( R in it0 iff R in LinOrders A ) by A1, A8; ::_thesis: verum
end;
hence  it0 = LinOrders A by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines LinOrders ARROW:def_3_:_
 for A being non empty set
for b2 being Subset of (LinPreorders A) holds
( b2 = LinOrders A iff for R being set holds
( R in b2 iff R is connected Order of A ) );

registration
let A be non empty set ;
cluster LinOrders A ->  non empty ;
coherence
 not LinOrders A is empty
proof
set R = the connected Order of A;
 the connected Order of A in LinOrders A by Def3;
hence  not LinOrders A is empty ; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
cluster  ->  Relation-like for Element of LinPreorders A;
coherence
 for b1 being Element of LinPreorders A holds b1 is Relation-like by Def1;
cluster  ->  Relation-like for Element of LinOrders A;
coherence
 for b1 being Element of LinOrders A holds b1 is Relation-like ;
end;


definition
let o be Relation;
let a, b be set ;
preda <=_ o,b means :Def4: :: ARROW:def 4
[a,b] in o;
end;

:: deftheorem Def4 defines <=_ ARROW:def_4_:_
 for o being Relation
for a, b being set holds
( a <=_ o,b iff [a,b] in o );

notation
let o be Relation;
let a, b be set ;
synonym b >=_ o,a for a <=_ o,b;
antonym b <_ o,a for a <=_ o,b;
antonym a >_ o,b for a <=_ o,b;
end;

theorem Th3: :: ARROW:3
for A being non empty set
for a being Element of A
for o being Element of LinPreorders A holds a <=_ o,a
proof
let A be non empty set ; ::_thesis: for a being Element of A
for o being Element of LinPreorders A holds a <=_ o,a
let a be Element of A; ::_thesis: for o being Element of LinPreorders A holds a <=_ o,a
let o be Element of LinPreorders A; ::_thesis: a <=_ o,a
thus  [a,a] in o by Def1; :: according to ARROW:def_4 ::_thesis: verum
end;

theorem Th4: :: ARROW:4
for A being non empty set
for a, b being Element of A
for o being Element of LinPreorders A holds
( a <=_ o,b or b <=_ o,a )
proof
let A be non empty set ; ::_thesis: for a, b being Element of A
for o being Element of LinPreorders A holds
( a <=_ o,b or b <=_ o,a )
let a, b be Element of A; ::_thesis: for o being Element of LinPreorders A holds
( a <=_ o,b or b <=_ o,a )
let o be Element of LinPreorders A; ::_thesis: ( a <=_ o,b or b <=_ o,a )
 ( [a,b] in o or [b,a] in o ) by Def1;
hence  ( a <=_ o,b or b <=_ o,a ) by Def4; ::_thesis: verum
end;

theorem Th5: :: ARROW:5
for A being non empty set
for a, b, c being Element of A
for o being Element of LinPreorders A st ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) holds
a <=_ o,c
proof
let A be non empty set ; ::_thesis: for a, b, c being Element of A
for o being Element of LinPreorders A st ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) holds
a <=_ o,c
let a, b, c be Element of A; ::_thesis: for o being Element of LinPreorders A st ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) holds
a <=_ o,c
let o be Element of LinPreorders A; ::_thesis: ( ( a <=_ o,b or a <_ o,b ) & ( b <=_ o,c or b <_ o,c ) implies a <=_ o,c )
assume  ( a <=_ o,b or a <_ o,b ) ; ::_thesis: ( ( not b <=_ o,c & not b <_ o,c ) or a <=_ o,c )
then  a <=_ o,b by Th4;
then A1: [a,b] in o by Def4;
assume  ( b <=_ o,c or b <_ o,c ) ; ::_thesis: a <=_ o,c
then  b <=_ o,c by Th4;
then  [b,c] in o by Def4;
hence  [a,c] in o by A1, Def1; :: according to ARROW:def_4 ::_thesis: verum
end;

theorem Th6: :: ARROW:6
for A being non empty set
for a, b being Element of A
for o99 being Element of LinOrders A st a <=_ o99,b & b <=_ o99,a holds
a = b
proof
let A be non empty set ; ::_thesis: for a, b being Element of A
for o99 being Element of LinOrders A st a <=_ o99,b & b <=_ o99,a holds
a = b
let a, b be Element of A; ::_thesis: for o99 being Element of LinOrders A st a <=_ o99,b & b <=_ o99,a holds
a = b
let o99 be Element of LinOrders A; ::_thesis: ( a <=_ o99,b & b <=_ o99,a implies a = b )
 ( [a,b] in o99 & [b,a] in o99 implies a = b ) by Def2;
hence  ( a <=_ o99,b & b <=_ o99,a implies a = b ) by Def4; ::_thesis: verum
end;

theorem Th7: :: ARROW:7
for A being non empty set
for a, b, c being Element of A st a <> b & b <> c & a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b & b <_ o,c )
proof
let A be non empty set ; ::_thesis: for a, b, c being Element of A st a <> b & b <> c & a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b & b <_ o,c )
let a, b, c be Element of A; ::_thesis: ( a <> b & b <> c & a <> c implies ex o being Element of LinPreorders A st
( a <_ o,b & b <_ o,c ) )
assume that
A1: ( a <> b & b <> c ) and
A2: a <> c ; ::_thesis: ex o being Element of LinPreorders A st
( a <_ o,b & b <_ o,c )
defpred S1[ set , set ] means ( ( $1 = a or $2 <> a ) & ( $1 <> c or $2 = c ) );
consider R being Relation of A such that
A3: for x, y being Element of A holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
A4: now__::_thesis:_for_x,_y_being_Element_of_A_holds_
(_[x,y]_in_R_or_[y,x]_in_R_)
let x, y be Element of A; ::_thesis: ( [x,y] in R or [y,x] in R )
 ( S1[x,y] or S1[y,x] ) by A2;
hence  ( [x,y] in R or [y,x] in R ) by A3; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_A_st_[x,y]_in_R_&_[y,z]_in_R_holds_
[x,z]_in_R
let x, y, z be Element of A; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume  ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R
then  ( S1[x,y] & S1[y,z] ) by A3;
hence  [x,z] in R by A3; ::_thesis: verum
end;
then reconsider o = R as Element of LinPreorders A by A4, Def1;
take  o ; ::_thesis: ( a <_ o,b & b <_ o,c )
 ( not [b,a] in R & not [c,b] in R ) by A1, A3;
hence  ( a <_ o,b & b <_ o,c ) by Def4; ::_thesis: verum
end;

theorem Th8: :: ARROW:8
for A being non empty set
for b being Element of A ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
b <_ o,a
proof
let A be non empty set ; ::_thesis: for b being Element of A ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
b <_ o,a
let b be Element of A; ::_thesis: ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
b <_ o,a
defpred S1[ set , set ] means ( $1 = b or $2 <> b );
consider R being Relation of A such that
A1: for x, y being Element of A holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
A2: now__::_thesis:_for_x,_y_being_Element_of_A_holds_
(_[x,y]_in_R_or_[y,x]_in_R_)
let x, y be Element of A; ::_thesis: ( [x,y] in R or [y,x] in R )
 ( S1[x,y] or S1[y,x] ) ;
hence  ( [x,y] in R or [y,x] in R ) by A1; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_A_st_[x,y]_in_R_&_[y,z]_in_R_holds_
[x,z]_in_R
let x, y, z be Element of A; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume that
A3: [x,y] in R and
A4: [y,z] in R ; ::_thesis: [x,z] in R
 S1[y,z] by A1, A4;
hence  [x,z] in R by A1, A3; ::_thesis: verum
end;
then reconsider o = R as Element of LinPreorders A by A2, Def1;
take  o ; ::_thesis: for a being Element of A st a <> b holds
b <_ o,a
let a be Element of A; ::_thesis: ( a <> b implies b <_ o,a )
assume  a <> b ; ::_thesis: b <_ o,a
then  not [a,b] in R by A1;
hence  b <_ o,a by Def4; ::_thesis: verum
end;

theorem Th9: :: ARROW:9
for A being non empty set
for b being Element of A ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
a <_ o,b
proof
let A be non empty set ; ::_thesis: for b being Element of A ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
a <_ o,b
let b be Element of A; ::_thesis: ex o being Element of LinPreorders A st
for a being Element of A st a <> b holds
a <_ o,b
defpred S1[ set , set ] means ( $1 <> b or $2 = b );
consider R being Relation of A such that
A1: for x, y being Element of A holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
A2: now__::_thesis:_for_x,_y_being_Element_of_A_holds_
(_[x,y]_in_R_or_[y,x]_in_R_)
let x, y be Element of A; ::_thesis: ( [x,y] in R or [y,x] in R )
 ( S1[x,y] or S1[y,x] ) ;
hence  ( [x,y] in R or [y,x] in R ) by A1; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_A_st_[x,y]_in_R_&_[y,z]_in_R_holds_
[x,z]_in_R
let x, y, z be Element of A; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume that
A3: [x,y] in R and
A4: [y,z] in R ; ::_thesis: [x,z] in R
 S1[x,y] by A1, A3;
hence  [x,z] in R by A1, A4; ::_thesis: verum
end;
then reconsider o = R as Element of LinPreorders A by A2, Def1;
take  o ; ::_thesis: for a being Element of A st a <> b holds
a <_ o,b
let a be Element of A; ::_thesis: ( a <> b implies a <_ o,b )
assume  a <> b ; ::_thesis: a <_ o,b
then  not [b,a] in R by A1;
hence  a <_ o,b by Def4; ::_thesis: verum
end;

theorem Th10: :: ARROW:10
for A being non empty set
for a, b, c being Element of A
for o9 being Element of LinPreorders A st a <> b & a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
proof
let A be non empty set ; ::_thesis: for a, b, c being Element of A
for o9 being Element of LinPreorders A st a <> b & a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
let a, b, c be Element of A; ::_thesis: for o9 being Element of LinPreorders A st a <> b & a <> c holds
ex o being Element of LinPreorders A st
( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
let o9 be Element of LinPreorders A; ::_thesis: ( a <> b & a <> c implies ex o being Element of LinPreorders A st
( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) ) )
assume A1: ( a <> b & a <> c ) ; ::_thesis: ex o being Element of LinPreorders A st
( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
defpred S1[ Element of A, Element of A] means ( $1 = a or ( $1 <=_ o9,$2 & $2 <> a ) );
consider R being Relation of A such that
A2: for x, y being Element of A holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
A3: now__::_thesis:_for_x,_y_being_Element_of_A_holds_
(_[x,y]_in_R_or_[y,x]_in_R_)
let x, y be Element of A; ::_thesis: ( [x,y] in R or [y,x] in R )
 ( S1[x,y] or S1[y,x] ) by Th4;
hence  ( [x,y] in R or [y,x] in R ) by A2; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_A_st_[x,y]_in_R_&_[y,z]_in_R_holds_
[x,z]_in_R
let x, y, z be Element of A; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume  ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R
then  ( S1[x,y] & S1[y,z] ) by A2;
then  S1[x,z] by Th5;
hence  [x,z] in R by A2; ::_thesis: verum
end;
then reconsider o = R as Element of LinPreorders A by A3, Def1;
take  o ; ::_thesis: ( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
A4: ( not [b,a] in R & not [c,a] in R ) by A1, A2;
A5: ( not [c,b] in R iff b <_ o9,c ) by A1, A2;
 ( not [b,c] in R iff c <_ o9,b ) by A1, A2;
hence  ( a <_ o,b & a <_ o,c & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) ) by A4, A5, Def4; ::_thesis: verum
end;

theorem Th11: :: ARROW:11
for A being non empty set
for a, b, c being Element of A
for o9 being Element of LinPreorders A st a <> b & a <> c holds
ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
proof
let A be non empty set ; ::_thesis: for a, b, c being Element of A
for o9 being Element of LinPreorders A st a <> b & a <> c holds
ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
let a, b, c be Element of A; ::_thesis: for o9 being Element of LinPreorders A st a <> b & a <> c holds
ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
let o9 be Element of LinPreorders A; ::_thesis: ( a <> b & a <> c implies ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) ) )
assume A1: ( a <> b & a <> c ) ; ::_thesis: ex o being Element of LinPreorders A st
( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
defpred S1[ Element of A, Element of A] means ( ( $1 <> a & $1 <=_ o9,$2 ) or $2 = a );
consider R being Relation of A such that
A2: for x, y being Element of A holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
A3: now__::_thesis:_for_x,_y_being_Element_of_A_holds_
(_[x,y]_in_R_or_[y,x]_in_R_)
let x, y be Element of A; ::_thesis: ( [x,y] in R or [y,x] in R )
 ( S1[x,y] or S1[y,x] ) by Th4;
hence  ( [x,y] in R or [y,x] in R ) by A2; ::_thesis: verum
end;
now__::_thesis:_for_x,_y,_z_being_Element_of_A_st_[x,y]_in_R_&_[y,z]_in_R_holds_
[x,z]_in_R
let x, y, z be Element of A; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume  ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R
then  ( S1[x,y] & S1[y,z] ) by A2;
then  S1[x,z] by Th5;
hence  [x,z] in R by A2; ::_thesis: verum
end;
then reconsider o = R as Element of LinPreorders A by A3, Def1;
take  o ; ::_thesis: ( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) )
A4: ( not [a,b] in R & not [a,c] in R ) by A1, A2;
A5: ( not [c,b] in R iff b <_ o9,c ) by A1, A2;
 ( not [b,c] in R iff c <_ o9,b ) by A1, A2;
hence  ( b <_ o,a & c <_ o,a & ( b <_ o,c implies b <_ o9,c ) & ( b <_ o9,c implies b <_ o,c ) & ( c <_ o,b implies c <_ o9,b ) & ( c <_ o9,b implies c <_ o,b ) ) by A4, A5, Def4; ::_thesis: verum
end;

theorem :: ARROW:12
for A being non empty set
for a, b being Element of A
for o, o9 being Element of LinOrders A holds
(  not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) ) )
proof
let A be non empty set ; ::_thesis: for a, b being Element of A
for o, o9 being Element of LinOrders A holds
(  not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) ) )
let a, b be Element of A; ::_thesis: for o, o9 being Element of LinOrders A holds
(  not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) ) )
let o, o9 be Element of LinOrders A; ::_thesis: (  not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) ) )
thus  not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) & not ( a <_ o,b iff a <_ o9,b ) ) ; ::_thesis: not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & not ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) ) )
assume A1: ( a <_ o,b iff a <_ o9,b ) ; ::_thesis: ( ( a <_ o,b implies a <_ o9,b ) & ( a <_ o9,b implies a <_ o,b ) & ( b <_ o,a implies b <_ o9,a ) & ( b <_ o9,a implies b <_ o,a ) )
hence  ( a <_ o,b iff a <_ o9,b ) ; ::_thesis: ( b <_ o,a iff b <_ o9,a )
hereby  ::_thesis: ( b <_ o9,a implies b <_ o,a )
assume A2: b <_ o,a ; ::_thesis: b <_ o9,a
then  a <> b by Th4;
hence  b <_ o9,a by A1, A2, Th4, Th6; ::_thesis: verum
end;
assume A3: b <_ o9,a ; ::_thesis: b <_ o,a
then  a <> b by Th4;
hence  b <_ o,a by A1, A3, Th4, Th6; ::_thesis: verum
end;

theorem Th13: :: ARROW:13
for A being non empty set
for o being Element of LinOrders A
for o9 being Element of LinPreorders A holds
( ( for a, b being Element of A st a <_ o,b holds
a <_ o9,b ) iff for a, b being Element of A holds
( a <_ o,b iff a <_ o9,b ) )
proof
let A be non empty set ; ::_thesis: for o being Element of LinOrders A
for o9 being Element of LinPreorders A holds
( ( for a, b being Element of A st a <_ o,b holds
a <_ o9,b ) iff for a, b being Element of A holds
( a <_ o,b iff a <_ o9,b ) )
let o be Element of LinOrders A; ::_thesis: for o9 being Element of LinPreorders A holds
( ( for a, b being Element of A st a <_ o,b holds
a <_ o9,b ) iff for a, b being Element of A holds
( a <_ o,b iff a <_ o9,b ) )
let o9 be Element of LinPreorders A; ::_thesis: ( ( for a, b being Element of A st a <_ o,b holds
a <_ o9,b ) iff for a, b being Element of A holds
( a <_ o,b iff a <_ o9,b ) )
hereby  ::_thesis: ( ( for a, b being Element of A holds
( a <_ o,b iff a <_ o9,b ) ) implies for a, b being Element of A st a <_ o,b holds
a <_ o9,b )
assume A1: for a, b being Element of A st a <_ o,b holds
a <_ o9,b ; ::_thesis: for a, b being Element of A holds
( b3 <_ o,b4 iff b3 <_ o9,b4 )
let a, b be Element of A; ::_thesis: ( b1 <_ o,b2 iff b1 <_ o9,b2 )
percases ( a <_ o,b or a = b or b <_ o,a ) by Th6;
suppose a <_ o,b ; ::_thesis: ( b1 <_ o,b2 iff b1 <_ o9,b2 )
hence  ( a <_ o,b iff a <_ o9,b ) by A1; ::_thesis: verum
end;
suppose a = b ; ::_thesis: ( b1 <_ o,b2 iff b1 <_ o9,b2 )
hence  ( a <_ o,b iff a <_ o9,b ) by Th3; ::_thesis: verum
end;
supposeA2: b <_ o,a ; ::_thesis: ( b1 <_ o,b2 iff b1 <_ o9,b2 )
then  b <_ o9,a by A1;
hence  ( a <_ o,b iff a <_ o9,b ) by A2, Th4; ::_thesis: verum
end;
end;
end;
thus  ( ( for a, b being Element of A holds
( a <_ o,b iff a <_ o9,b ) ) implies for a, b being Element of A st a <_ o,b holds
a <_ o9,b ) ; ::_thesis: verum
end;

begin


theorem Th14: :: ARROW:14
for A, N being non empty finite set
for f being Function of (Funcs (N,(LinPreorders A))),(LinPreorders A) st ( 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 ) & ( 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 ) ) & card A >= 3 holds
ex n being Element of N st
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b
proof
let A, N be non empty finite set ; ::_thesis: for f being Function of (Funcs (N,(LinPreorders A))),(LinPreorders A) st ( 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 ) & ( 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 ) ) & card A >= 3 holds
ex n being Element of N st
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b
let f be Function of (Funcs (N,(LinPreorders A))),(LinPreorders A); ::_thesis: ( ( 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 ) & ( 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 ) ) & card A >= 3 implies ex n being Element of N st
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b )
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: ex n being Element of N st
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b
defpred S1[ 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 S1[p . i,b] ) holds
S1[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 S1[p . i,b] ) & not S1[f . p,b] ) ; ::_thesis: contradiction
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 S1[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 )
proof
percases ( a9 <> c9 or a9 = c9 ) ;
supposeA10: a9 <> c9 ; ::_thesis: ex a, c being Element of A st
( a <> b & b <> c & a <> c & a <=_ f . p,b & b <=_ f . p,c )
take  a9 ; ::_thesis: ex c being Element of A st
( a9 <> b & b <> c & a9 <> c & a9 <=_ f . p,b & b <=_ f . p,c )
take  c9 ; ::_thesis: ( a9 <> b & b <> c9 & a9 <> c9 & a9 <=_ f . p,b & b <=_ f . p,c9 )
thus  ( a9 <> b & b <> c9 & a9 <> c9 & a9 <=_ f . p,b & b <=_ f . p,c9 ) by A8, A9, A10; ::_thesis: verum
end;
supposeA11: a9 = c9 ; ::_thesis: ex a, c being Element of A st
( a <> b & b <> c & a <> c & a <=_ f . p,b & b <=_ f . p,c )
consider d being Element of A such that
A12: ( d <> b & d <> a9 ) by A3, Th2;
percases ( d <=_ f . p,b or b <=_ f . p,d ) by Th4;
supposeA13: d <=_ f . p,b ; ::_thesis: ex a, c being Element of A st
( a <> b & b <> c & a <> c & a <=_ f . p,b & b <=_ f . p,c )
take  d ; ::_thesis: ex c being Element of A st
( d <> b & b <> c & d <> c & d <=_ f . p,b & b <=_ f . p,c )
take  c9 ; ::_thesis: ( d <> b & b <> c9 & d <> c9 & d <=_ f . p,b & b <=_ f . p,c9 )
thus  ( d <> b & b <> c9 & d <> c9 & d <=_ f . p,b & b <=_ f . p,c9 ) by A9, A11, A12, A13; ::_thesis: verum
end;
supposeA14: b <=_ f . p,d ; ::_thesis: ex a, c being Element of A st
( a <> b & b <> c & a <> c & a <=_ f . p,b & b <=_ f . p,c )
take  a9 ; ::_thesis: ex c being Element of A st
( a9 <> b & b <> c & a9 <> c & a9 <=_ f . p,b & b <=_ f . p,c )
take  d ; ::_thesis: ( a9 <> b & b <> d & a9 <> d & a9 <=_ f . p,b & b <=_ f . p,d )
thus  ( a9 <> b & b <> d & a9 <> d & a9 <=_ f . p,b & b <=_ f . p,d ) by A8, A12, A14; ::_thesis: verum
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 S2[ 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 S2[i,o]
proof
let i be Element of N; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
percases ( for c being Element of A st c <> b holds
b <_ p . i,c or for a being Element of A st a <> b holds
a <_ p . i,b ) by A7;
suppose for c being Element of A st c <> b holds
b <_ p . i,c ; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
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: S2[i,o]
thus  S2[i,o] by A19, A20, Th4, Th5; ::_thesis: verum
end;
suppose for a being Element of A st a <> b holds
a <_ p . i,b ; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
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: S2[i,o]
thus  S2[i,o] by A21, A22, Th4, Th5; ::_thesis: verum
end;
end;
end;
consider p9 being Function of N,(LinPreorders A) such that
A23: for i being Element of N holds S2[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: verum
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 S1[pI . i,b] ) & ( for i being Element of N holds S1[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
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: 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 S1[pI . i,b] ) & ( for i being Element of N holds S1[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 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 ) )
proof
let k0 be Nat; ::_thesis: 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 ) )
defpred S2[ 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 S2[i,o]
proof
let i be Element of N; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
consider k being set  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;
percases ( k < k0 or k >= k0 ) ;
supposeA33: k < k0 ; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
take  oII ; ::_thesis: S2[i,oII]
thus  S2[i,oII] by A31, A32, A33; ::_thesis: verum
end;
supposeA34: k >= k0 ; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
take  oI ; ::_thesis: S2[i,oI]
thus  S2[i,oI] by A31, A32, A34; ::_thesis: verum
end;
end;
end;
consider p being Function of N,(LinPreorders A) such that
A35: for i being Element of N holds S2[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: ( ( 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 ) )
thus  for k being Nat st k in dom t & k < k0 holds
p . (t . k) = oII ::_thesis: for k being Nat st k in dom t & k >= k0 holds
p . (t . k) = oI
proof
let k be Nat; ::_thesis: ( k in dom t & k < k0 implies p . (t . k) = oII )
assume that
A36: k in dom t and
A37: k < k0 ; ::_thesis: p . (t . k) = oII
reconsider i = t . k as Element of N by A36, PARTFUN1:4;
 S2[i,p . i] by A35;
hence  p . (t . k) = oII by A26, A36, A37, FUNCT_1:def_4; ::_thesis: verum
end;
let k be Nat; ::_thesis: ( k in dom t & k >= k0 implies p . (t . k) = oI )
assume that
A38: k in dom t and
A39: k >= k0 ; ::_thesis: p . (t . k) = oI
reconsider i = t . k as Element of N by A38, PARTFUN1:4;
 S2[i,p . i] by A35;
hence  p . (t . k) = oI by A26, A38, A39, FUNCT_1:def_4; ::_thesis: verum
end;
defpred S2[ 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: S2[kII9]
proof
let p be Element of Funcs (N,(LinPreorders A)); ::_thesis: ( ( for k being Nat st k in dom t & k < kII9 holds
p . (t . k) = oII ) & ( for k being Nat st k in dom t & k >= kII9 holds
p . (t . k) = oI ) implies for a being Element of A st a <> b holds
a <_ f . p,b )
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: for a being Element of A st a <> b holds
a <_ f . p,b
let a be Element of A; ::_thesis: ( a <> b implies a <_ f . p,b )
assume A42: a <> b ; ::_thesis: a <_ f . p,b
 for i being Element of N holds a <_ p . i,b
proof
let i be Element of N; ::_thesis: a <_ p . i,b
consider k being set  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: verum
end;
hence  a <_ f . p,b by A1; ::_thesis: verum
end;
then A45: ex kII9 being Nat st S2[kII9] ;
consider kII being Nat such that
A46: ( S2[kII] & ( for k0 being Nat st S2[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
proof
assume A50: kII <= 1 ; ::_thesis: contradiction
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
proof
let i be Element of N; ::_thesis: b <_ pII . i,a
consider k being set  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: verum
end;
A55: a <_ f . pII,b by A46, A47, A48, A51;
 b <_ f . pII,a by A1, A52;
hence  contradiction by A55, Th4; ::_thesis: verum
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: 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 S1[pI . i,b] ) & ( for i being Element of N holds S1[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 ) )
take  pI ; ::_thesis: ex 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 S1[pI . i,b] ) & ( for i being Element of N holds S1[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 ) )
take  pII ; ::_thesis: ( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for i being Element of N holds S1[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 ) )
thus  for i being Element of N st i <> nb holds
pI . i = pII . i ::_thesis: ( ( for i being Element of N holds S1[pI . i,b] ) & ( for i being Element of N holds S1[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
let i be Element of N; ::_thesis: ( i <> nb implies pI . i = pII . i )
assume A63: i <> nb ; ::_thesis: pI . i = pII . i
consider k being set  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;
percases ( k < kI or k > kI ) by A63, A65, XXREAL_0:1;
suppose k < kI ; ::_thesis: pI . i = pII . i
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: verum
end;
suppose k > kI ; ::_thesis: pI . i = pII . i
then  ( k >= kII & pI . i = oI ) by A56, A61, A64, A65, INT_1:7;
hence  pI . i = pII . i by A48, A64, A65; ::_thesis: verum
end;
end;
end;
thus A66: for i being Element of N holds S1[pI . i,b] ::_thesis: ( ( for i being Element of N holds S1[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
let i be Element of N; ::_thesis: S1[pI . i,b]
 ex k being set 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  S1[pI . i,b] by A27, A28; ::_thesis: verum
end;
thus  for i being Element of N holds S1[pII . i,b] ::_thesis: ( ( 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
let i be Element of N; ::_thesis: S1[pII . i,b]
 ex k being set 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  S1[pII . i,b] by A27, A28; ::_thesis: verum
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: ( ( 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 ) )
 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: ( ( 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 ) )
thus  for a being Element of A st a <> b holds
b <_ f . pI,a by A4, A62, A66; ::_thesis: for a being Element of A st a <> b holds
a <_ f . pII,b
thus  for a being Element of A st a <> b holds
a <_ f . pII,b by A46, A47, A48; ::_thesis: verum
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 S1[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: 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 S1[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 ) )
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 S1[pI . i,b] and
A70: for i being Element of N holds S1[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: 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 S1[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 ) )
take  pI ; ::_thesis: ex 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 S1[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 ) )
take  pII ; ::_thesis: ( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[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 ) )
thus  ( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[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: 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 p be Element of Funcs (N,(LinPreorders A)); ::_thesis: for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c
let a, c be Element of A; ::_thesis: ( a <> b & c <> b & a <_ p . nb,c implies a <_ f . p,c )
assume that
A74: a <> b and
A75: c <> b and
A76: a <_ p . nb,c ; ::_thesis: a <_ f . p,c
A77: a <> c by A76, Th3;
defpred S2[ 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 S2[i,o]
proof
let i be Element of N; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
percases ( i = nb or i <> nb ) ;
supposeA79: i = nb ; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
consider o being Element of LinPreorders A such that
A80: ( a <_ o,b & b <_ o,c ) by A74, A75, A77, Th7;
take  o ; ::_thesis: S2[i,o]
thus  S2[i,o] by A76, A79, A80, Th4, Th5; ::_thesis: verum
end;
supposeA81: i <> nb ; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
percases ( for d being Element of A st d <> b holds
b <_ pII . i,d or for d being Element of A st d <> b holds
d <_ pII . i,b ) by A70;
suppose for d being Element of A st d <> b holds
b <_ pII . i,d ; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
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: S2[i,o]
thus  S2[i,o] by A74, A81, A82, A83; ::_thesis: verum
end;
suppose for d being Element of A st d <> b holds
d <_ pII . i,b ; ::_thesis: ex o being Element of LinPreorders A st S2[i,o]
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: S2[i,o]
thus  S2[i,o] by A74, A81, A84, A85; ::_thesis: verum
end;
end;
end;
end;
end;
consider pIII being Function of N,(LinPreorders A) such that
A86: for i being Element of N holds S2[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 ) )
proof
let i be Element of N; ::_thesis: ( ( 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 ) )
percases ( i = nb or i <> nb ) ;
suppose i = nb ; ::_thesis: ( ( 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 ) )
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: verum
end;
supposeA87: i <> nb ; ::_thesis: ( ( 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 ) )
percases ( for d being Element of A st d <> b holds
b <_ pII . i,d or for d being Element of A st d <> b holds
d <_ pII . i,b ) by A70;
suppose for d being Element of A st d <> b holds
b <_ pII . i,d ; ::_thesis: ( ( 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 ) )
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: verum
end;
suppose for d being Element of A st d <> b holds
d <_ pII . i,b ; ::_thesis: ( ( 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 ) )
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: verum
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 ) )
proof
let i be Element of N; ::_thesis: ( ( 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 ) )
percases ( i = nb or i <> nb ) ;
suppose i = nb ; ::_thesis: ( ( 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 ) )
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: verum
end;
supposeA89: i <> nb ; ::_thesis: ( ( 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 ) )
percases ( for d being Element of A st d <> b holds
b <_ pII . i,d or for d being Element of A st d <> b holds
d <_ pII . i,b ) by A70;
supposeA90: for d being Element of A st d <> b holds
b <_ pII . i,d ; ::_thesis: ( ( 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 ) )
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: verum
end;
supposeA92: for d being Element of A st d <> b holds
d <_ pII . i,b ; ::_thesis: ( ( 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 ) )
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: verum
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: verum
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 S1[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: for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . nb,b holds
a <_ f . p,b
let p be Element of Funcs (N,(LinPreorders A)); ::_thesis: for a, b being Element of A st a <_ p . nb,b holds
a <_ f . p,b
let a, a9 be Element of A; ::_thesis: ( a <_ p . nb,a9 implies a <_ f . p,a9 )
assume A98: a <_ p . nb,a9 ; ::_thesis: a <_ f . p,a9
then A99: a <> a9 by Th4;
percases ( ( a <> the Element of A & a9 <> the Element of A ) or a = the Element of A or a9 = the Element of A ) ;
suppose ( a <> the Element of A & a9 <> the Element of A ) ; ::_thesis: a <_ f . p,a9
hence  a <_ f . p,a9 by A97, A98; ::_thesis: verum
end;
supposeA100: ( a = the Element of A or a9 = the Element of A ) ; ::_thesis: a <_ f . p,a9
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 S1[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
proof
percases ( a = the Element of A or a9 = the Element of A ) by A100;
supposeA103: a = the Element of A ; ::_thesis: nc = nb
assume A104: nc <> nb ; ::_thesis: contradiction
 ( 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: verum
end;
supposeA105: a9 = the Element of A ; ::_thesis: nc = nb
assume A106: nc <> nb ; ::_thesis: contradiction
 ( 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: verum
end;
end;
end;
hence  a <_ f . p,a9 by A98, A101, A102; ::_thesis: verum
end;
end;
end;


theorem :: ARROW:15
for A, N being non empty finite set
for f being Function of (Funcs (N,(LinOrders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinOrders 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 ) & ( for p, p9 being Element of Funcs (N,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 holds
ex n being Element of N st
for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
proof
let A, N be non empty finite set ; ::_thesis: for f being Function of (Funcs (N,(LinOrders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinOrders 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 ) & ( for p, p9 being Element of Funcs (N,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 holds
ex n being Element of N st
for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
let f be Function of (Funcs (N,(LinOrders A))),(LinPreorders A); ::_thesis: ( ( for p being Element of Funcs (N,(LinOrders 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 ) & ( for p, p9 being Element of Funcs (N,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 implies ex n being Element of N st
for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b ) )
assume that
A1: for p being Element of Funcs (N,(LinOrders 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,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) and
A3: card A >= 3 ; ::_thesis: ex n being Element of N st
for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
set o = the Element of LinOrders A;
defpred S1[ Element of LinPreorders A, Element of A, Element of A] means ( $2 <=_ $1,$3 & ( $2 <_ $1,$3 or $2 <=_ the Element of LinOrders A,$3 ) );
defpred S2[ Element of LinPreorders A, Element of LinOrders A] means  for a, b being Element of A holds
( S1[$1,a,b] iff a <=_ $2,b );
A4: for o9 being Element of LinPreorders A ex o1 being Element of LinOrders A st S2[o9,o1]
proof
let o9 be Element of LinPreorders A; ::_thesis: ex o1 being Element of LinOrders A st S2[o9,o1]
defpred S3[ Element of A, Element of A] means S1[o9,$1,$2];
consider o1 being Relation of A such that
A5: for a, b being Element of A holds
( [a,b] in o1 iff S3[a,b] ) from RELSET_1:sch_2();
A6: now__::_thesis:_for_a,_b_being_Element_of_A_holds_
(_[a,b]_in_o1_or_[b,a]_in_o1_)
let a, b be Element of A; ::_thesis: ( [a,b] in o1 or [b,a] in o1 )
 ( S3[a,b] or S3[b,a] ) by Th4;
hence  ( [a,b] in o1 or [b,a] in o1 ) by A5; ::_thesis: verum
end;
now__::_thesis:_for_a,_b,_c_being_Element_of_A_st_[a,b]_in_o1_&_[b,c]_in_o1_holds_
[a,c]_in_o1
let a, b, c be Element of A; ::_thesis: ( [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 )
 ( S3[a,b] & S3[b,c] implies S3[a,c] ) by Th5;
hence  ( [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 ) by A5; ::_thesis: verum
end;
then reconsider o1 = o1 as Element of LinPreorders A by A6, Def1;
now__::_thesis:_for_a,_b_being_Element_of_A_st_[a,b]_in_o1_&_[b,a]_in_o1_holds_
a_=_b
let a, b be Element of A; ::_thesis: ( [a,b] in o1 & [b,a] in o1 implies a = b )
 ( S3[a,b] & S3[b,a] implies a = b ) by Th6;
hence  ( [a,b] in o1 & [b,a] in o1 implies a = b ) by A5; ::_thesis: verum
end;
then reconsider o1 = o1 as Element of LinOrders A by Def2;
take  o1 ; ::_thesis: S2[o9,o1]
let a, b be Element of A; ::_thesis: ( S1[o9,a,b] iff a <=_ o1,b )
 ( [a,b] in o1 iff S3[a,b] ) by A5;
hence  ( S1[o9,a,b] iff a <=_ o1,b ) by Def4; ::_thesis: verum
end;
defpred S3[ Element of Funcs (N,(LinPreorders A)), Element of Funcs (N,(LinOrders A))] means  for i being Element of N holds S2[$1 . i,$2 . i];
A7: for q being Element of Funcs (N,(LinPreorders A))
for p, p9 being Element of Funcs (N,(LinOrders A)) st S3[q,p] & S3[q,p9] holds
p = p9
proof
let q be Element of Funcs (N,(LinPreorders A)); ::_thesis: for p, p9 being Element of Funcs (N,(LinOrders A)) st S3[q,p] & S3[q,p9] holds
p = p9
let p, p9 be Element of Funcs (N,(LinOrders A)); ::_thesis: ( S3[q,p] & S3[q,p9] implies p = p9 )
assume that
A8: S3[q,p] and
A9: S3[q,p9] ; ::_thesis: p = p9
let i be Element of N; :: according to FUNCT_2:def_8 ::_thesis: p . i = p9 . i
reconsider pi = p . i as Relation of A by Def1;
reconsider pi9 = p9 . i as Relation of A by Def1;
now__::_thesis:_for_a,_b_being_Element_of_A_holds_
(_[a,b]_in_p_._i_iff_[a,b]_in_p9_._i_)
let a, b be Element of A; ::_thesis: ( [a,b] in p . i iff [a,b] in p9 . i )
A10: ( S1[q . i,a,b] iff a <=_ p . i,b ) by A8;
 ( S1[q . i,a,b] iff a <=_ p9 . i,b ) by A9;
hence  ( [a,b] in p . i iff [a,b] in p9 . i ) by A10, Def4; ::_thesis: verum
end;
then  pi = pi9 by RELSET_1:def_2;
hence  p . i = p9 . i ; ::_thesis: verum
end;
A11: for q being Element of Funcs (N,(LinPreorders A)) ex p being Element of Funcs (N,(LinOrders A)) st S3[q,p]
proof
let q be Element of Funcs (N,(LinPreorders A)); ::_thesis: ex p being Element of Funcs (N,(LinOrders A)) st S3[q,p]
defpred S4[ Element of N, Element of LinOrders A] means S2[q . $1,$2];
A12: for i being Element of N ex o1 being Element of LinOrders A st S4[i,o1] by A4;
consider p being Function of N,(LinOrders A) such that
A13: for i being Element of N holds S4[i,p . i] from FUNCT_2:sch_3(A12);
reconsider p = p as Element of Funcs (N,(LinOrders A)) by FUNCT_2:8;
take  p ; ::_thesis: S3[q,p]
thus  S3[q,p] by A13; ::_thesis: verum
end;
defpred S4[ Element of Funcs (N,(LinPreorders A)), Element of LinPreorders A] means  ex p being Element of Funcs (N,(LinOrders A)) st
( S3[$1,p] & f . p = $2 );
A14: for q being Element of Funcs (N,(LinPreorders A)) ex o9 being Element of LinPreorders A st S4[q,o9]
proof
let q be Element of Funcs (N,(LinPreorders A)); ::_thesis: ex o9 being Element of LinPreorders A st S4[q,o9]
consider p being Element of Funcs (N,(LinOrders A)) such that
A15: S3[q,p] by A11;
take  f . p ; ::_thesis: S4[q,f . p]
thus  S4[q,f . p] by A15; ::_thesis: verum
end;
consider f9 being Function of (Funcs (N,(LinPreorders A))),(LinPreorders A) such that
A16: for q being Element of Funcs (N,(LinPreorders A)) holds S4[q,f9 . q] from FUNCT_2:sch_3(A14);
A17: for q being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds a <_ q . i,b ) holds
a <_ f9 . q,b
proof
let q be Element of Funcs (N,(LinPreorders A)); ::_thesis: for a, b being Element of A st ( for i being Element of N holds a <_ q . i,b ) holds
a <_ f9 . q,b
let a, b be Element of A; ::_thesis: ( ( for i being Element of N holds a <_ q . i,b ) implies a <_ f9 . q,b )
assume A18: for i being Element of N holds a <_ q . i,b ; ::_thesis: a <_ f9 . q,b
consider p being Element of Funcs (N,(LinOrders A)) such that
A19: S3[q,p] and
A20: f . p = f9 . q by A16;
now__::_thesis:_for_i_being_Element_of_N_holds_a_<__p_._i,b
let i be Element of N; ::_thesis: a <_ p . i,b
 not S1[q . i,b,a] by A18;
hence  a <_ p . i,b by A19; ::_thesis: verum
end;
hence  a <_ f9 . q,b by A1, A20; ::_thesis: verum
end;
now__::_thesis:_for_q,_q9_being_Element_of_Funcs_(N,(LinPreorders_A))
for_a,_b_being_Element_of_A_st_(_for_i_being_Element_of_N_holds_
(_(_a_<__q_._i,b_implies_a_<__q9_._i,b_)_&_(_a_<__q9_._i,b_implies_a_<__q_._i,b_)_&_(_b_<__q_._i,a_implies_b_<__q9_._i,a_)_&_(_b_<__q9_._i,a_implies_b_<__q_._i,a_)_)_)_holds_
(_a_<__f9_._q,b_iff_a_<__f9_._q9,b_)
let q, q9 be Element of Funcs (N,(LinPreorders A)); ::_thesis: for a, b being Element of A st ( for i being Element of N holds
( ( a <_ q . i,b implies a <_ q9 . i,b ) & ( a <_ q9 . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q9 . i,a ) & ( b <_ q9 . i,a implies b <_ q . i,a ) ) ) holds
( a <_ f9 . q,b iff a <_ f9 . q9,b )
let a, b be Element of A; ::_thesis: ( ( for i being Element of N holds
( ( a <_ q . i,b implies a <_ q9 . i,b ) & ( a <_ q9 . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q9 . i,a ) & ( b <_ q9 . i,a implies b <_ q . i,a ) ) ) implies ( a <_ f9 . q,b iff a <_ f9 . q9,b ) )
assume A21: for i being Element of N holds
( ( a <_ q . i,b implies a <_ q9 . i,b ) & ( a <_ q9 . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q9 . i,a ) & ( b <_ q9 . i,a implies b <_ q . i,a ) ) ; ::_thesis: ( a <_ f9 . q,b iff a <_ f9 . q9,b )
consider p being Element of Funcs (N,(LinOrders A)) such that
A22: S3[q,p] and
A23: f . p = f9 . q by A16;
consider p9 being Element of Funcs (N,(LinOrders A)) such that
A24: S3[q9,p9] and
A25: f . p9 = f9 . q9 by A16;
 for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b )
proof
let i be Element of N; ::_thesis: ( a <_ p . i,b iff a <_ p9 . i,b )
 ( S1[q . i,b,a] iff S1[q9 . i,b,a] ) by A21;
hence  ( a <_ p . i,b iff a <_ p9 . i,b ) by A22, A24; ::_thesis: verum
end;
hence  ( a <_ f9 . q,b iff a <_ f9 . q9,b ) by A2, A23, A25; ::_thesis: verum
end;
then consider n being Element of N such that
A26: for q being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ q . n,b holds
a <_ f9 . q,b by A3, A17, Th14;
take  n ; ::_thesis: for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
let p be Element of Funcs (N,(LinOrders A)); ::_thesis: for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
now__::_thesis:_for_a,_b_being_Element_of_A_st_a_<__p_._n,b_holds_
a_<__f_._p,b
 rng p c= LinOrders A by RELAT_1:def_19;
then  ( dom p = N & rng p c= LinPreorders A ) by FUNCT_2:def_1, XBOOLE_1:1;
then reconsider q = p as Element of Funcs (N,(LinPreorders A)) by FUNCT_2:def_2;
A27: S3[q,p]
proof
let i be Element of N; ::_thesis: S2[q . i,p . i]
let a, b be Element of A; ::_thesis: ( S1[q . i,a,b] iff a <=_ p . i,b )
 ( a <_ p . i,b or a = b or a >_ p . i,b ) by Th6;
hence  ( S1[q . i,a,b] iff a <=_ p . i,b ) by Th4; ::_thesis: verum
end;
A28: ex p9 being Element of Funcs (N,(LinOrders A)) st
( S3[q,p9] & f . p9 = f9 . q ) by A16;
let a, b be Element of A; ::_thesis: ( a <_ p . n,b implies a <_ f . p,b )
assume  a <_ p . n,b ; ::_thesis: a <_ f . p,b
then  a <_ f9 . q,b by A26;
hence  a <_ f . p,b by A7, A27, A28; ::_thesis: verum
end;
hence  for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b ) by Th13; ::_thesis: verum
end;