:: 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;