:: ORDERS_3 semantic presentation

begin

definition
let IT be RelStr ;
attrIT is discrete  means :Def1: :: ORDERS_3:def 1
 the InternalRel of IT = id the carrier of IT;
end;

:: deftheorem Def1 defines discrete ORDERS_3:def_1_:_
 for IT being RelStr holds
( IT is discrete iff the InternalRel of IT = id the carrier of IT );

registration
cluster non empty strict V65() reflexive transitive antisymmetric discrete for RelStr ;
existence
 ex b1 being Poset st
( b1 is strict & b1 is discrete & not b1 is empty )
proof
set A = the non empty set ;
reconsider R = id the non empty set as Relation of the non empty set ;
reconsider R = R as Order of the non empty set ;
take  RelStr(# the non empty set ,R #) ; ::_thesis: ( RelStr(# the non empty set ,R #) is strict & RelStr(# the non empty set ,R #) is discrete & not RelStr(# the non empty set ,R #) is empty )
thus  ( RelStr(# the non empty set ,R #) is strict & RelStr(# the non empty set ,R #) is discrete & not RelStr(# the non empty set ,R #) is empty ) by Def1; ::_thesis: verum
end;
end;

registration
cluster RelStr(# {},(id {}) #) ->  empty ;
coherence
 RelStr(# {},(id {}) #) is empty ;
let P be empty RelStr ;
cluster the InternalRel of P ->  empty ;
coherence
 the InternalRel of P is empty ;
end;

Lm1:  for P being RelStr st P is empty holds
P is discrete
proof
let P be RelStr ; ::_thesis: ( P is empty implies P is discrete )
assume  P is empty ; ::_thesis: P is discrete
then  ( the carrier of P = {} & the InternalRel of P = {} ) ;
hence  P is discrete by Def1, RELAT_1:55; ::_thesis: verum
end;

registration
cluster empty  ->  discrete for RelStr ;
coherence
 for b1 being RelStr st b1 is empty holds
b1 is discrete by Lm1;
end;

definition
let P be RelStr ;
let IT be Subset of P;
attrIT is disconnected  means :Def2: :: ORDERS_3:def 2
 ex A, B being Subset of P st
( A <> {} & B <> {} & IT = A \/ B & A misses B & the InternalRel of P = ( the InternalRel of P |_2 A) \/ ( the InternalRel of P |_2 B) );
end;

:: deftheorem Def2 defines disconnected ORDERS_3:def_2_:_
 for P being RelStr
for IT being Subset of P holds
( IT is disconnected iff ex A, B being Subset of P st
( A <> {} & B <> {} & IT = A \/ B & A misses B & the InternalRel of P = ( the InternalRel of P |_2 A) \/ ( the InternalRel of P |_2 B) ) );

notation
let P be RelStr ;
let IT be Subset of P;
antonym  connected IT for  disconnected ;
end;

definition
let IT be RelStr ;
attrIT is disconnected  means :Def3: :: ORDERS_3:def 3
 [#] IT is disconnected ;
end;

:: deftheorem Def3 defines disconnected ORDERS_3:def_3_:_
 for IT being RelStr holds
( IT is disconnected iff [#] IT is disconnected );

notation
let IT be RelStr ;
antonym  connected IT for  disconnected ;
end;


theorem :: ORDERS_3:1
for DP being non empty discrete RelStr
for x, y being Element of DP holds
( x <= y iff x = y )
proof
let DP be non empty discrete RelStr ; ::_thesis: for x, y being Element of DP holds
( x <= y iff x = y )
let x, y be Element of DP; ::_thesis: ( x <= y iff x = y )
hereby  ::_thesis: ( x = y implies x <= y )
assume  x <= y ; ::_thesis: x = y
then  [x,y] in the InternalRel of DP by ORDERS_2:def_5;
then  [x,y] in id the carrier of DP by Def1;
hence  x = y by RELAT_1:def_10; ::_thesis: verum
end;
assume  x = y ; ::_thesis: x <= y
then  [x,y] in id the carrier of DP by RELAT_1:def_10;
then  [x,y] in the InternalRel of DP by Def1;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;

theorem :: ORDERS_3:2
for R being Relation
for a being set st R is Order of {a} holds
R = id {a}
proof
let R be Relation; ::_thesis: for a being set st R is Order of {a} holds
R = id {a}
let a be set ; ::_thesis: ( R is Order of {a} implies R = id {a} )
assume A1: R is Order of {a} ; ::_thesis: R = id {a}
then A2: R <> {} ;
 R c= [:{a},{a}:] by A1;
then  R c= {[a,a]} by ZFMISC_1:29;
then  R = {[a,a]} by A2, ZFMISC_1:33;
hence  R = id {a} by SYSREL:13; ::_thesis: verum
end;

theorem :: ORDERS_3:3
for T being non empty RelStr
for a being Element of T st T is reflexive & [#] T = {a} holds
T is discrete
proof
let T be non empty RelStr ; ::_thesis: for a being Element of T st T is reflexive & [#] T = {a} holds
T is discrete
let a be Element of T; ::_thesis: ( T is reflexive & [#] T = {a} implies T is discrete )
assume A1: T is reflexive ; ::_thesis: ( not [#] T = {a} or T is discrete )
set R = the InternalRel of T;
assume A2: [#] T = {a} ; ::_thesis: T is discrete
 the InternalRel of T = id {a}
proof
A3: id {a} = {[a,a]} by SYSREL:13;
 the InternalRel of T c= [:{a},{a}:] by A2;
hence  the InternalRel of T c= id {a} by A3, ZFMISC_1:29; :: according to XBOOLE_0:def_10 ::_thesis: id {a} c= the InternalRel of T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in id {a} or x in the InternalRel of T )
assume  x in id {a} ; ::_thesis: x in the InternalRel of T
then A4: x = [a,a] by A3, TARSKI:def_1;
 a >= a by A1, ORDERS_2:1;
hence  x in the InternalRel of T by A4, ORDERS_2:def_5; ::_thesis: verum
end;
hence  T is discrete by A2, Def1; ::_thesis: verum
end;

theorem Th4: :: ORDERS_3:4
for T being non empty RelStr
for a being set st [#] T = {a} holds
T is connected
proof
let T be non empty RelStr ; ::_thesis: for a being set st [#] T = {a} holds
T is connected
let a be set ; ::_thesis: ( [#] T = {a} implies T is connected )
reconsider OT = [#] T as non empty set ;
assume A1: [#] T = {a} ; ::_thesis: T is connected
A2: for Z, Z9 being non empty Subset of OT holds not Z misses Z9
proof
let Z, Z9 be non empty Subset of OT; ::_thesis: not Z misses Z9
 Z = {a} by A1, ZFMISC_1:33;
hence  not Z misses Z9 by A1, ZFMISC_1:33; ::_thesis: verum
end;
 [#] T is connected
proof
assume  [#] T is disconnected ; ::_thesis: contradiction
then  ex A, B being Subset of T st
( A <> {} & B <> {} & [#] T = A \/ B & A misses B & the InternalRel of T = ( the InternalRel of T |_2 A) \/ ( the InternalRel of T |_2 B) ) by Def2;
hence  contradiction by A2; ::_thesis: verum
end;
hence  T is connected by Def3; ::_thesis: verum
end;

theorem Th5: :: ORDERS_3:5
for DP being non empty discrete Poset st ex a, b being Element of DP st a <> b holds
DP is disconnected
proof
let DP be non empty discrete Poset; ::_thesis: ( ex a, b being Element of DP st a <> b implies DP is disconnected )
given a, b being Element of DP such that A1: a <> b ; ::_thesis: DP is disconnected
 not b in {a} by A1, TARSKI:def_1;
then reconsider A = the carrier of DP \ {a} as non empty Subset of DP by XBOOLE_0:def_5;
reconsider B = {a} as non empty Subset of DP ;
A2: ( the carrier of DP = ( the carrier of DP \ {a}) \/ {a} & the carrier of DP \ {a} misses {a} ) by XBOOLE_1:45, XBOOLE_1:79;
 the InternalRel of DP c= [:A,A:] \/ [:B,B:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the InternalRel of DP or x in [:A,A:] \/ [:B,B:] )
assume A3: x in the InternalRel of DP ; ::_thesis: x in [:A,A:] \/ [:B,B:]
then consider x1, x2 being set  such that
A4: x = [x1,x2] by RELAT_1:def_1;
A5: x in id the carrier of DP by A3, Def1;
then A6: x1 = x2 by A4, RELAT_1:def_10;
percases ( x1 in A or not x1 in A ) ;
supposeA7: x1 in A ; ::_thesis: x in [:A,A:] \/ [:B,B:]
A8: [:A,A:] c= [:A,A:] \/ [:B,B:] by XBOOLE_1:7;
 [x1,x1] in [:A,A:] by A7, ZFMISC_1:87;
hence  x in [:A,A:] \/ [:B,B:] by A4, A6, A8; ::_thesis: verum
end;
supposeA9: not x1 in A ; ::_thesis: x in [:A,A:] \/ [:B,B:]
 x1 in the carrier of DP by A5, A4, RELAT_1:def_10;
then  x1 in the carrier of DP \ A by A9, XBOOLE_0:def_5;
then  x1 in the carrier of DP /\ B by XBOOLE_1:48;
then  x1 in B by XBOOLE_1:28;
then A10: [x1,x1] in [:B,B:] by ZFMISC_1:87;
 [:B,B:] c= [:A,A:] \/ [:B,B:] by XBOOLE_1:7;
hence  x in [:A,A:] \/ [:B,B:] by A4, A6, A10; ::_thesis: verum
end;
end;
end;
then A11: the InternalRel of DP = the InternalRel of DP /\ ([:A,A:] \/ [:B,B:]) by XBOOLE_1:28;
 ( the InternalRel of DP |_2 A = the InternalRel of DP /\ [:A,A:] & the InternalRel of DP |_2 B = the InternalRel of DP /\ [:B,B:] ) by WELLORD1:def_6;
then  the InternalRel of DP = ( the InternalRel of DP |_2 A) \/ ( the InternalRel of DP |_2 B) by A11, XBOOLE_1:23;
then  [#] DP is disconnected by A2, Def2;
hence  DP is disconnected by Def3; ::_thesis: verum
end;

registration
cluster non empty strict V65() reflexive transitive antisymmetric connected for RelStr ;
existence
 ex b1 being non empty Poset st
( b1 is strict & b1 is connected )
proof
set x = the set ;
reconsider A = RelStr(# { the set },(id { the set }) #) as non empty Poset ;
 [#] A = { the set } ;
then  A is connected by Th4;
hence  ex b1 being non empty Poset st
( b1 is strict & b1 is connected ) ; ::_thesis: verum
end;
cluster non empty strict V65() reflexive transitive antisymmetric discrete disconnected for RelStr ;
existence
 ex b1 being non empty Poset st
( b1 is strict & b1 is disconnected & b1 is discrete )
proof
 ex Y being non empty Poset st
( Y is strict & Y is disconnected & Y is discrete )
proof
reconsider A = RelStr(# {1,2},(id {1,2}) #) as non empty Poset ;
reconsider A = A as non empty discrete Poset by Def1;
take  A ; ::_thesis: ( A is strict & A is disconnected & A is discrete )
 ex a, b being Element of A st a <> b
proof
set a = 1;
set b = 2;
reconsider a = 1, b = 2 as Element of A by TARSKI:def_2;
take  a ; ::_thesis: ex b being Element of A st a <> b
take  b ; ::_thesis: a <> b
thus  a <> b ; ::_thesis: verum
end;
hence  ( A is strict & A is disconnected & A is discrete ) by Th5; ::_thesis: verum
end;
hence  ex b1 being non empty Poset st
( b1 is strict & b1 is disconnected & b1 is discrete ) ; ::_thesis: verum
end;
end;

begin

definition
let IT be set ;
attrIT is POSet_set-like  means :Def4: :: ORDERS_3:def 4
 for a being set st a in IT holds
a is non empty Poset;
end;

:: deftheorem Def4 defines POSet_set-like ORDERS_3:def_4_:_
 for IT being set holds
( IT is POSet_set-like iff for a being set st a in IT holds
a is non empty Poset );

registration
cluster non empty POSet_set-like for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is POSet_set-like )
proof
set P = the non empty Poset;
set A = { the non empty Poset};
take  { the non empty Poset} ; ::_thesis: ( not { the non empty Poset} is empty & { the non empty Poset} is POSet_set-like )
 for a being set st a in { the non empty Poset} holds
a is non empty Poset by TARSKI:def_1;
hence  ( not { the non empty Poset} is empty & { the non empty Poset} is POSet_set-like ) by Def4; ::_thesis: verum
end;
end;

definition
mode POSet_set is POSet_set-like set ;
end;

definition
let P be non empty POSet_set;
:: original: Element
redefine mode Element of P ->  non empty Poset;
coherence
 for b1 being Element of P holds b1 is non empty Poset by Def4;
end;

definition
let L1, L2 be RelStr ;
let f be Function of L1,L2;
attrf is monotone  means :Def5: :: ORDERS_3:def 5
 for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a <= b;
end;

:: deftheorem Def5 defines monotone ORDERS_3:def_5_:_
 for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is monotone iff for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a <= b );

Lm2:  for A, B, C being non empty RelStr
for f being Function of A,B
for g being Function of B,C st f is monotone & g is monotone holds
ex gf being Function of A,C st
( gf = g * f & gf is monotone )
proof
let A, B, C be non empty RelStr ; ::_thesis: for f being Function of A,B
for g being Function of B,C st f is monotone & g is monotone holds
ex gf being Function of A,C st
( gf = g * f & gf is monotone )
let f be Function of A,B; ::_thesis: for g being Function of B,C st f is monotone & g is monotone holds
ex gf being Function of A,C st
( gf = g * f & gf is monotone )
let g be Function of B,C; ::_thesis: ( f is monotone & g is monotone implies ex gf being Function of A,C st
( gf = g * f & gf is monotone ) )
assume that
A1: f is monotone and
A2: g is monotone ; ::_thesis: ex gf being Function of A,C st
( gf = g * f & gf is monotone )
reconsider gf = g * f as Function of A,C ;
take  gf ; ::_thesis: ( gf = g * f & gf is monotone )
now__::_thesis:_for_p1,_p2_being_Element_of_A_st_p1_<=_p2_holds_
for_r1,_r2_being_Element_of_C_st_r1_=_gf_._p1_&_r2_=_gf_._p2_holds_
r1_<=_r2
let p1, p2 be Element of A; ::_thesis: ( p1 <= p2 implies for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds
r1 <= r2 )
reconsider p19 = f . p1, p29 = f . p2 as Element of B ;
 dom f = the carrier of A by FUNCT_2:def_1;
then A3: ( g . (f . p1) = (g * f) . p1 & g . (f . p2) = (g * f) . p2 ) by FUNCT_1:13;
assume  p1 <= p2 ; ::_thesis: for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds
r1 <= r2
then A4: p19 <= p29 by A1, Def5;
let r1, r2 be Element of C; ::_thesis: ( r1 = gf . p1 & r2 = gf . p2 implies r1 <= r2 )
assume  ( r1 = gf . p1 & r2 = gf . p2 ) ; ::_thesis: r1 <= r2
hence  r1 <= r2 by A2, A3, A4, Def5; ::_thesis: verum
end;
hence  ( gf = g * f & gf is monotone ) by Def5; ::_thesis: verum
end;

   Lm3:  for T being non empty RelStr holds id T is monotone
proof
let T be non empty RelStr ; ::_thesis: id T is monotone
set IT = id T;
let p1, p2 be Element of T; :: according to ORDERS_3:def_5 ::_thesis: ( p1 <= p2 implies for a, b being Element of T st a = (id T) . p1 & b = (id T) . p2 holds
a <= b )
assume A1: p1 <= p2 ; ::_thesis: for a, b being Element of T st a = (id T) . p1 & b = (id T) . p2 holds
a <= b
let r1, r2 be Element of T; ::_thesis: ( r1 = (id T) . p1 & r2 = (id T) . p2 implies r1 <= r2 )
reconsider p19 = p1 as Element of T ;
A2: (id T) . p19 = p19 by FUNCT_1:18;
assume  ( r1 = (id T) . p1 & r2 = (id T) . p2 ) ; ::_thesis: r1 <= r2
hence  r1 <= r2 by A1, A2, FUNCT_1:18; ::_thesis: verum
end;

definition
let A, B be RelStr ;
func MonFuncs (A,B) ->  set  means :Def6: :: ORDERS_3:def 6
 for a being set holds
( a in it iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) );
existence
 ex b1 being set st
for a being set holds
( a in b1 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) )
proof
defpred S1[ set ] means  ex f being Function of A,B st
( f = $1 & f is monotone );
consider AB being set  such that
A1: for a being set holds
( a in AB iff ( a in Funcs ( the carrier of A, the carrier of B) & S1[a] ) ) from XBOOLE_0:sch_1();
take  AB ; ::_thesis: for a being set holds
( a in AB iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) )
thus  for a being set holds
( a in AB iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ::_thesis: verum
proof
let a be set ; ::_thesis: ( a in AB iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) )
hereby  ::_thesis: ( ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) implies a in AB )
assume A2: a in AB ; ::_thesis: ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone )
then consider f being Function of A,B such that
A3: ( f = a & f is monotone ) by A1;
take f = f; ::_thesis: ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone )
thus  ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A1, A2, A3; ::_thesis: verum
end;
given f being Function of A,B such that A4: ( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ; ::_thesis: a in AB
thus  a in AB by A1, A4; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being set st ( for a being set holds
( a in b1 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) & ( for a being set holds
( a in b2 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for a being set holds
( a in A1 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) & ( for a being set holds
( a in A2 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ) implies A1 = A2 )
assume that
A5: for a being set holds
( a in A1 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) and
A6: for a being set holds
( a in A2 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) ; ::_thesis: A1 = A2
 for a being set st a in A2 holds
a in A1
proof
let a be set ; ::_thesis: ( a in A2 implies a in A1 )
assume  a in A2 ; ::_thesis: a in A1
then  ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A6;
hence  a in A1 by A5; ::_thesis: verum
end;
then A7: A2 c= A1 by TARSKI:def_3;
 for a being set st a in A1 holds
a in A2
proof
let a be set ; ::_thesis: ( a in A1 implies a in A2 )
assume  a in A1 ; ::_thesis: a in A2
then  ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by A5;
hence  a in A2 by A6; ::_thesis: verum
end;
then  A1 c= A2 by TARSKI:def_3;
hence  A1 = A2 by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines MonFuncs ORDERS_3:def_6_:_
 for A, B being RelStr
for b3 being set holds
( b3 = MonFuncs (A,B) iff for a being set holds
( a in b3 iff ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) ) );

theorem Th6: :: ORDERS_3:6
for A, B, C being non empty RelStr
for f, g being Function st f in MonFuncs (A,B) & g in MonFuncs (B,C) holds
g * f in MonFuncs (A,C)
proof
let A, B, C be non empty RelStr ; ::_thesis: for f, g being Function st f in MonFuncs (A,B) & g in MonFuncs (B,C) holds
g * f in MonFuncs (A,C)
let f, g be Function; ::_thesis: ( f in MonFuncs (A,B) & g in MonFuncs (B,C) implies g * f in MonFuncs (A,C) )
assume that
A1: f in MonFuncs (A,B) and
A2: g in MonFuncs (B,C) ; ::_thesis: g * f in MonFuncs (A,C)
consider f9 being Function of A,B such that
A3: f = f9 and
 f9 in Funcs ( the carrier of A, the carrier of B) and
A4: f9 is monotone by A1, Def6;
consider g9 being Function of B,C such that
A5: g = g9 and
 g9 in Funcs ( the carrier of B, the carrier of C) and
A6: g9 is monotone by A2, Def6;
consider gf being Function of A,C such that
A7: ( gf = g9 * f9 & gf is monotone ) by A4, A6, Lm2;
 gf in Funcs ( the carrier of A, the carrier of C) by FUNCT_2:8;
hence  g * f in MonFuncs (A,C) by A3, A5, A7, Def6; ::_thesis: verum
end;

theorem Th7: :: ORDERS_3:7
for T being non empty RelStr holds id the carrier of T in MonFuncs (T,T)
proof
let T be non empty RelStr ; ::_thesis: id the carrier of T in MonFuncs (T,T)
reconsider IT = id T as Function of the carrier of T, the carrier of T ;
reconsider IT9 = IT as Function of T,T ;
 ( id T is monotone & IT9 in Funcs ( the carrier of T, the carrier of T) ) by Lm3, FUNCT_2:9;
hence  id the carrier of T in MonFuncs (T,T) by Def6; ::_thesis: verum
end;

registration
let T be non empty RelStr ;
cluster MonFuncs (T,T) ->  non empty ;
coherence
 not MonFuncs (T,T) is empty by Th7;
end;

definition
let X be set ;
func Carr X ->  set  means :Def7: :: ORDERS_3:def 7
 for a being set holds
( a in it iff ex s being 1-sorted st
( s in X & a = the carrier of s ) );
existence
 ex b1 being set st
for a being set holds
( a in b1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) )
proof
defpred S1[ set , set ] means  ex s being 1-sorted st
( s = $1 & $2 = the carrier of s );
A1: for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z ;
consider CX being set  such that
A2: for x being set holds
( x in CX iff ex y being set st
( y in X & S1[y,x] ) ) from TARSKI:sch_1(A1);
take  CX ; ::_thesis: for a being set holds
( a in CX iff ex s being 1-sorted st
( s in X & a = the carrier of s ) )
let x be set ; ::_thesis: ( x in CX iff ex s being 1-sorted st
( s in X & x = the carrier of s ) )
 ( x in CX iff ex s being 1-sorted st
( s in X & x = the carrier of s ) )
proof
thus  ( x in CX implies ex s being 1-sorted st
( s in X & x = the carrier of s ) ) ::_thesis: ( ex s being 1-sorted st
( s in X & x = the carrier of s ) implies x in CX )
proof
assume  x in CX ; ::_thesis: ex s being 1-sorted st
( s in X & x = the carrier of s )
then consider y being set  such that
A3: y in X and
A4: ex s being 1-sorted st
( s = y & x = the carrier of s ) by A2;
consider s being 1-sorted  such that
A5: s = y and
 x = the carrier of s by A4;
take  s ; ::_thesis: ( s in X & x = the carrier of s )
thus  ( s in X & x = the carrier of s ) by A3, A4, A5; ::_thesis: verum
end;
given s being 1-sorted  such that A6: ( s in X & x = the carrier of s ) ; ::_thesis: x in CX
thus  x in CX by A2, A6; ::_thesis: verum
end;
hence  ( x in CX iff ex s being 1-sorted st
( s in X & x = the carrier of s ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for a being set holds
( a in b1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) & ( for a being set holds
( a in b2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) holds
b1 = b2
proof
let C1, C2 be set ; ::_thesis: ( ( for a being set holds
( a in C1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) & ( for a being set holds
( a in C2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) implies C1 = C2 )
assume that
A7: for a being set holds
( a in C1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) and
A8: for a being set holds
( a in C2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ; ::_thesis: C1 = C2
 for a being set holds
( a in C1 iff a in C2 )
proof
let a be set ; ::_thesis: ( a in C1 iff a in C2 )
thus  ( a in C1 implies a in C2 ) ::_thesis: ( a in C2 implies a in C1 )
proof
assume  a in C1 ; ::_thesis: a in C2
then  ex s being 1-sorted st
( s in X & a = the carrier of s ) by A7;
hence  a in C2 by A8; ::_thesis: verum
end;
thus  ( a in C2 implies a in C1 ) ::_thesis: verum
proof
assume  a in C2 ; ::_thesis: a in C1
then  ex s being 1-sorted st
( s in X & a = the carrier of s ) by A8;
hence  a in C1 by A7; ::_thesis: verum
end;
end;
hence  C1 = C2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Carr ORDERS_3:def_7_:_
 for X, b2 being set holds
( b2 = Carr X iff for a being set holds
( a in b2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) );

Lm4:  for P being non empty POSet_set
for A being Element of P holds the carrier of A in Carr P
by Def7;

registration
let P be non empty POSet_set;
cluster Carr P ->  non empty ;
coherence
 not Carr P is empty by Lm4;
end;

theorem :: ORDERS_3:8
for f being 1-sorted holds Carr {f} = { the carrier of f}
proof
let f be 1-sorted ; ::_thesis: Carr {f} = { the carrier of f}
thus  Carr {f} c= { the carrier of f} :: according to XBOOLE_0:def_10 ::_thesis: { the carrier of f} c= Carr {f}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Carr {f} or a in { the carrier of f} )
assume  a in Carr {f} ; ::_thesis: a in { the carrier of f}
then consider s being 1-sorted  such that
A1: s in {f} and
A2: a = the carrier of s by Def7;
 s = f by A1, TARSKI:def_1;
hence  a in { the carrier of f} by A2, TARSKI:def_1; ::_thesis: verum
end;
A3: f in {f} by TARSKI:def_1;
thus  { the carrier of f} c= Carr {f} ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { the carrier of f} or a in Carr {f} )
assume  a in { the carrier of f} ; ::_thesis: a in Carr {f}
then  a = the carrier of f by TARSKI:def_1;
hence  a in Carr {f} by A3, Def7; ::_thesis: verum
end;
end;

theorem :: ORDERS_3:9
for f, g being 1-sorted holds Carr {f,g} = { the carrier of f, the carrier of g}
proof
let f, g be 1-sorted ; ::_thesis: Carr {f,g} = { the carrier of f, the carrier of g}
thus  Carr {f,g} c= { the carrier of f, the carrier of g} :: according to XBOOLE_0:def_10 ::_thesis: { the carrier of f, the carrier of g} c= Carr {f,g}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Carr {f,g} or a in { the carrier of f, the carrier of g} )
assume  a in Carr {f,g} ; ::_thesis: a in { the carrier of f, the carrier of g}
then consider s being 1-sorted  such that
A1: s in {f,g} and
A2: a = the carrier of s by Def7;
percases ( s = f or s = g ) by A1, TARSKI:def_2;
suppose s = f ; ::_thesis: a in { the carrier of f, the carrier of g}
hence  a in { the carrier of f, the carrier of g} by A2, TARSKI:def_2; ::_thesis: verum
end;
suppose s = g ; ::_thesis: a in { the carrier of f, the carrier of g}
hence  a in { the carrier of f, the carrier of g} by A2, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
thus  { the carrier of f, the carrier of g} c= Carr {f,g} ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { the carrier of f, the carrier of g} or a in Carr {f,g} )
A3: f in {f,g} by TARSKI:def_2;
A4: g in {f,g} by TARSKI:def_2;
assume A5: a in { the carrier of f, the carrier of g} ; ::_thesis: a in Carr {f,g}
percases ( a = the carrier of f or a = the carrier of g ) by A5, TARSKI:def_2;
suppose a = the carrier of f ; ::_thesis: a in Carr {f,g}
hence  a in Carr {f,g} by A3, Def7; ::_thesis: verum
end;
suppose a = the carrier of g ; ::_thesis: a in Carr {f,g}
hence  a in Carr {f,g} by A4, Def7; ::_thesis: verum
end;
end;
end;
end;

theorem Th10: :: ORDERS_3:10
for P being non empty POSet_set
for A, B being Element of P holds MonFuncs (A,B) c= Funcs (Carr P)
proof
let P be non empty POSet_set; ::_thesis: for A, B being Element of P holds MonFuncs (A,B) c= Funcs (Carr P)
let A, B be Element of P; ::_thesis: MonFuncs (A,B) c= Funcs (Carr P)
reconsider CA = the carrier of A, CB = the carrier of B as Element of Carr P by Def7;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MonFuncs (A,B) or x in Funcs (Carr P) )
assume  x in MonFuncs (A,B) ; ::_thesis: x in Funcs (Carr P)
then A1: ex g being Function of A,B st
( x = g & g in Funcs ( the carrier of A, the carrier of B) & g is monotone ) by Def6;
 Funcs (CA,CB) c= Funcs (Carr P) by ENS_1:2;
hence  x in Funcs (Carr P) by A1; ::_thesis: verum
end;

theorem Th11: :: ORDERS_3:11
for A, B being RelStr holds MonFuncs (A,B) c= Funcs ( the carrier of A, the carrier of B)
proof
let A, B be RelStr ; ::_thesis: MonFuncs (A,B) c= Funcs ( the carrier of A, the carrier of B)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in MonFuncs (A,B) or a in Funcs ( the carrier of A, the carrier of B) )
assume  a in MonFuncs (A,B) ; ::_thesis: a in Funcs ( the carrier of A, the carrier of B)
then  ex f being Function of A,B st
( a = f & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by Def6;
hence  a in Funcs ( the carrier of A, the carrier of B) ; ::_thesis: verum
end;

registration
let A, B be non empty Poset;
cluster MonFuncs (A,B) ->  functional ;
coherence
 MonFuncs (A,B) is functional
proof
reconsider X = MonFuncs (A,B) as Subset of (Funcs ( the carrier of A, the carrier of B)) by Th11;
 X is functional ;
hence  MonFuncs (A,B) is functional ; ::_thesis: verum
end;
end;

definition
let P be non empty POSet_set;
func POSCat P ->  strict with_triple-like_morphisms Category means :: ORDERS_3:def 8
( the carrier of it = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of it
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) );
existence
 ex b1 being strict with_triple-like_morphisms Category st
( the carrier of b1 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b1
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) )
proof
deffunc H1( Function, Function) ->  set = $1 * $2;
defpred S1[ Element of P, Element of P, set ] means $3 in MonFuncs ($1,$2);
A1: for a, b, c being Element of P
for f, g being Element of Funcs (Carr P) st S1[a,b,f] & S1[b,c,g] holds
( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] )
proof
let a, b, c be Element of P; ::_thesis: for f, g being Element of Funcs (Carr P) st S1[a,b,f] & S1[b,c,g] holds
( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] )
let f, g be Element of Funcs (Carr P); ::_thesis: ( S1[a,b,f] & S1[b,c,g] implies ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) )
assume  ( f in MonFuncs (a,b) & g in MonFuncs (b,c) ) ; ::_thesis: ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] )
then A2: g * f in MonFuncs (a,c) by Th6;
 MonFuncs (a,c) c= Funcs (Carr P) by Th10;
hence  ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) by A2; ::_thesis: verum
end;
A3: for a being Element of P ex f being Element of Funcs (Carr P) st
( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) )
proof
let a be Element of P; ::_thesis: ex f being Element of Funcs (Carr P) st
( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) )
set f = id the carrier of a;
 ( MonFuncs (a,a) c= Funcs (Carr P) & id the carrier of a in MonFuncs (a,a) ) by Th7, Th10;
then reconsider f = id the carrier of a as Element of Funcs (Carr P) ;
take  f ; ::_thesis: ( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) )
now__::_thesis:_for_b_being_Element_of_P
for_g_being_Element_of_Funcs_(Carr_P)_holds_
(_(_g_in_MonFuncs_(a,b)_implies_g_*_f_=_g_)_&_(_g_in_MonFuncs_(b,a)_implies_f_*_g_=_g_)_)
let b be Element of P; ::_thesis: for g being Element of Funcs (Carr P) holds
( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) )
let g be Element of Funcs (Carr P); ::_thesis: ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) )
A4: ( g in MonFuncs (b,a) implies f * g = g )
proof
assume  g in MonFuncs (b,a) ; ::_thesis: f * g = g
then  ex g9 being Function of b,a st
( g9 = g & g9 in Funcs ( the carrier of b, the carrier of a) & g9 is monotone ) by Def6;
then reconsider g = g as Function of the carrier of b, the carrier of a ;
 rng g c= the carrier of a ;
hence  f * g = g by RELAT_1:53; ::_thesis: verum
end;
 ( g in MonFuncs (a,b) implies g * f = g )
proof
assume  g in MonFuncs (a,b) ; ::_thesis: g * f = g
then  ex g9 being Function of a,b st
( g9 = g & g9 in Funcs ( the carrier of a, the carrier of b) & g9 is monotone ) by Def6;
then reconsider g = g as Function of the carrier of a, the carrier of b ;
 dom g = the carrier of a by FUNCT_2:def_1;
hence  g * f = g by RELAT_1:51; ::_thesis: verum
end;
hence  ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) by A4; ::_thesis: verum
end;
hence  ( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) by Th7; ::_thesis: verum
end;
A5: for a, b, c, d being Element of P
for f, g, h being Element of Funcs (Carr P) st S1[a,b,f] & S1[b,c,g] & S1[c,d,h] holds
H1(h,H1(g,f)) = H1(H1(h,g),f) by RELAT_1:36;
 ex C being strict with_triple-like_morphisms Category st
( the carrier of C = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st S1[a,b,f] holds
[[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) ) from CAT_5:sch_1(A1, A3, A5);
hence  ex b1 being strict with_triple-like_morphisms Category st
( the carrier of b1 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b1
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b1
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) & the carrier of b2 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b2
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) holds
b1 = b2
proof
deffunc H1( Element of Funcs (Carr P), Element of Funcs (Carr P)) ->  set = $1 * $2;
defpred S1[ Element of P, Element of P, Element of Funcs (Carr P)] means $3 in MonFuncs ($1,$2);
A6: now__::_thesis:_for_a_being_Element_of_P_ex_f_being_Element_of_Funcs_(Carr_P)_st_
(_S1[a,a,f]_&_(_for_b_being_Element_of_P
for_g_being_Element_of_Funcs_(Carr_P)_holds_
(_(_S1[a,b,g]_implies_H1(g,f)_=_g_)_&_(_S1[b,a,g]_implies_H1(f,g)_=_g_)_)_)_)
let a be Element of P; ::_thesis: ex f being Element of Funcs (Carr P) st
( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) )
thus  ex f being Element of Funcs (Carr P) st
( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) ::_thesis: verum
proof
set f = id the carrier of a;
A7: id the carrier of a in MonFuncs (a,a) by Th7;
 MonFuncs (a,a) c= Funcs (Carr P) by Th10;
then reconsider f = id the carrier of a as Element of Funcs (Carr P) by A7;
now__::_thesis:_for_b_being_Element_of_P
for_g_being_Element_of_Funcs_(Carr_P)_holds_
(_(_g_in_MonFuncs_(a,b)_implies_g_*_f_=_g_)_&_(_g_in_MonFuncs_(b,a)_implies_f_*_g_=_g_)_)
let b be Element of P; ::_thesis: for g being Element of Funcs (Carr P) holds
( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) )
let g be Element of Funcs (Carr P); ::_thesis: ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) )
A8: ( g in MonFuncs (b,a) implies f * g = g )
proof
assume  g in MonFuncs (b,a) ; ::_thesis: f * g = g
then  ex g9 being Function of b,a st
( g9 = g & g9 in Funcs ( the carrier of b, the carrier of a) & g9 is monotone ) by Def6;
then reconsider g = g as Function of the carrier of b, the carrier of a ;
 rng g c= the carrier of a ;
hence  f * g = g by RELAT_1:53; ::_thesis: verum
end;
 ( g in MonFuncs (a,b) implies g * f = g )
proof
assume  g in MonFuncs (a,b) ; ::_thesis: g * f = g
then  ex g9 being Function of a,b st
( g9 = g & g9 in Funcs ( the carrier of a, the carrier of b) & g9 is monotone ) by Def6;
then reconsider g = g as Function of the carrier of a, the carrier of b ;
 dom g = the carrier of a by FUNCT_2:def_1;
hence  g * f = g by RELAT_1:51; ::_thesis: verum
end;
hence  ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) by A8; ::_thesis: verum
end;
hence  ex f being Element of Funcs (Carr P) st
( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) by A7; ::_thesis: verum
end;
end;
thus  for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st S1[a,b,f] holds
[[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C1
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) & the carrier of C2 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st S1[a,b,f] holds
[[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C2
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) holds
C1 = C2 from CAT_5:sch_2(A6); ::_thesis: verum
end;
end;

:: deftheorem  defines POSCat ORDERS_3:def_8_:_
 for P being non empty POSet_set
for b2 being strict with_triple-like_morphisms Category holds
( b2 = POSCat P iff ( the carrier of b2 = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b2
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) ) );

begin

scheme :: ORDERS_3:sch 1
AltCatEx{ F1() ->  non empty set , F2( set , set ) ->  functional set } :
 ex C being strict AltCatStr st
( the carrier of C = F1() & ( for i, j being Element of F1() holds
( the Arrows of C . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) )
provided
A1: for i, j, k being Element of F1()
for f, g being Function st f in F2(i,j) & g in F2(j,k) holds
g * f in F2(i,k)
proof
deffunc H1( set , set , set ) ->  set = FuncComp (F2($1,$2),F2($2,$3));
consider M being ManySortedSet of [:F1(),F1():] such that
A2: for i, j being Element of F1() holds M . (i,j) = F2(i,j) from ALTCAT_1:sch_2();
consider c being ManySortedSet of [:F1(),F1(),F1():] such that
A3: for i, j, k being Element of F1() holds c . (i,j,k) = H1(i,j,k) from ALTCAT_1:sch_4();
 c is Function-yielding
proof
let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in dom c or c . i is set )
assume  i in dom c ; ::_thesis: c . i is set
then  i in [:F1(),F1(),F1():] ;
then consider x1, x2, x3 being set  such that
A4: ( x1 in F1() & x2 in F1() & x3 in F1() ) and
A5: i = [x1,x2,x3] by MCART_1:68;
c . i = c . (x1,x2,x3) by A5, MULTOP_1:def_1
.= FuncComp (F2(x1,x2),F2(x2,x3)) by A3, A4 ;
hence  c . i is set ; ::_thesis: verum
end;
then reconsider c = c as ManySortedFunction of [:F1(),F1(),F1():] ;
now__::_thesis:_for_i_being_set_st_i_in_[:F1(),F1(),F1():]_holds_
c_._i_is_Function_of_({|M,M|}_._i),({|M|}_._i)
let i be set ; ::_thesis: ( i in [:F1(),F1(),F1():] implies c . i is Function of ({|M,M|} . i),({|M|} . i) )
assume  i in [:F1(),F1(),F1():] ; ::_thesis: c . i is Function of ({|M,M|} . i),({|M|} . i)
then consider x1, x2, x3 being set  such that
A6: x1 in F1() and
A7: x2 in F1() and
A8: x3 in F1() and
A9: i = [x1,x2,x3] by MCART_1:68;
 M . (x1,x2) = F2(x1,x2) by A2, A6, A7;
then A10: [:F2(x2,x3),F2(x1,x2):] = [:(M . (x2,x3)),(M . (x1,x2)):] by A2, A7, A8
.= {|M,M|} . (x1,x2,x3) by A6, A7, A8, ALTCAT_1:def_4
.= {|M,M|} . i by A9, MULTOP_1:def_1 ;
A11: {|M|} . i = {|M|} . (x1,x2,x3) by A9, MULTOP_1:def_1
.= M . (x1,x3) by A6, A7, A8, ALTCAT_1:def_3 ;
A12: now__::_thesis:_(_{|M,M|}_._i_<>_{}_implies_{|M|}_._i_<>_{}_)
assume  {|M,M|} . i <> {} ; ::_thesis: {|M|} . i <> {}
then consider j being set  such that
A13: j in [:F2(x2,x3),F2(x1,x2):] by A10, XBOOLE_0:def_1;
consider j1, j2 being set  such that
A14: j1 in F2(x2,x3) and
A15: j2 in F2(x1,x2) and
 j = [j1,j2] by A13, ZFMISC_1:84;
reconsider j2 = j2 as Function by A15;
reconsider j1 = j1 as Function by A14;
 j1 * j2 in F2(x1,x3) by A1, A6, A7, A8, A14, A15;
hence  {|M|} . i <> {} by A2, A6, A8, A11; ::_thesis: verum
end;
A16: c . i = c . (x1,x2,x3) by A9, MULTOP_1:def_1
.= FuncComp (F2(x1,x2),F2(x2,x3)) by A3, A6, A7, A8 ;
then reconsider ci = c . i as Function ;
A17: dom ci = [:F2(x2,x3),F2(x1,x2):] by A16, PARTFUN1:def_2;
 rng (FuncComp (F2(x1,x2),F2(x2,x3))) c= F2(x1,x3)
proof
set F = FuncComp (F2(x1,x2),F2(x2,x3));
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng (FuncComp (F2(x1,x2),F2(x2,x3))) or i in F2(x1,x3) )
assume  i in rng (FuncComp (F2(x1,x2),F2(x2,x3))) ; ::_thesis: i in F2(x1,x3)
then consider j being set  such that
A18: j in dom (FuncComp (F2(x1,x2),F2(x2,x3))) and
A19: i = (FuncComp (F2(x1,x2),F2(x2,x3))) . j by FUNCT_1:def_3;
consider f, g being Function such that
A20: j = [g,f] and
A21: (FuncComp (F2(x1,x2),F2(x2,x3))) . j = g * f by A18, ALTCAT_1:def_9;
 ( g in F2(x2,x3) & f in F2(x1,x2) ) by A18, A20, ZFMISC_1:87;
hence  i in F2(x1,x3) by A1, A6, A7, A8, A19, A21; ::_thesis: verum
end;
then  rng ci c= {|M|} . i by A2, A6, A8, A16, A11;
hence  c . i is Function of ({|M,M|} . i),({|M|} . i) by A17, A10, A12, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
then reconsider c = c as BinComp of M by PBOOLE:def_15;
set C = AltCatStr(# F1(),M,c #);
take  AltCatStr(# F1(),M,c #) ; ::_thesis: ( the carrier of AltCatStr(# F1(),M,c #) = F1() & ( for i, j being Element of F1() holds
( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) )
thus  the carrier of AltCatStr(# F1(),M,c #) = F1() ; ::_thesis: for i, j being Element of F1() holds
( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) )
let i, j be Element of F1(); ::_thesis: ( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) )
thus  the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) by A2; ::_thesis: for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k))
let i, j, k be Element of F1(); ::_thesis: the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k))
thus  the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) by A3; ::_thesis: verum
end;

scheme :: ORDERS_3:sch 2
AltCatUniq{ F1() ->  non empty set , F2( set , set ) ->  functional set } :
 for C1, C2 being strict AltCatStr st the carrier of C1 = F1() & ( for i, j being Element of F1() holds
( the Arrows of C1 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) & the carrier of C2 = F1() & ( for i, j being Element of F1() holds
( the Arrows of C2 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) holds
C1 = C2
proof
let C1, C2 be strict AltCatStr ; ::_thesis: ( the carrier of C1 = F1() & ( for i, j being Element of F1() holds
( the Arrows of C1 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) & the carrier of C2 = F1() & ( for i, j being Element of F1() holds
( the Arrows of C2 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) implies C1 = C2 )
assume that
A1: the carrier of C1 = F1() and
A2: for i, j being Element of F1() holds
( the Arrows of C1 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) and
A3: the carrier of C2 = F1() and
A4: for i, j being Element of F1() holds
( the Arrows of C2 . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of C2 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ; ::_thesis: C1 = C2
A5: now__::_thesis:_for_i,_j,_k_being_set_st_i_in_F1()_&_j_in_F1()_&_k_in_F1()_holds_
the_Comp_of_C1_._(i,j,k)_=_the_Comp_of_C2_._(i,j,k)
let i, j, k be set ; ::_thesis: ( i in F1() & j in F1() & k in F1() implies the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) )
assume A6: ( i in F1() & j in F1() & k in F1() ) ; ::_thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
hence  the Comp of C1 . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) by A2
.= the Comp of C2 . (i,j,k) by A4, A6 ;
::_thesis: verum
end;
now__::_thesis:_for_i,_j_being_Element_of_F1()_holds_the_Arrows_of_C1_._(i,j)_=_the_Arrows_of_C2_._(i,j)
let i, j be Element of F1(); ::_thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
thus  the Arrows of C1 . (i,j) = F2(i,j) by A2
.= the Arrows of C2 . (i,j) by A4 ; ::_thesis: verum
end;
then  the Arrows of C1 = the Arrows of C2 by A1, A3, ALTCAT_1:7;
hence  C1 = C2 by A1, A3, A5, ALTCAT_1:8; ::_thesis: verum
end;

definition
let P be non empty POSet_set;
func POSAltCat P ->  strict AltCatStr  means :Def9: :: ORDERS_3:def 9
( the carrier of it = P & ( for i, j being Element of P holds
( the Arrows of it . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of it . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) );
existence
 ex b1 being strict AltCatStr st
( the carrier of b1 = P & ( for i, j being Element of P holds
( the Arrows of b1 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b1 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) )
proof
A1: for i, j, k being Element of P
for f, g being Function st f in MonFuncs (i,j) & g in MonFuncs (j,k) holds
g * f in MonFuncs (i,k) by Th6;
thus  ex C being strict AltCatStr st
( the carrier of C = P & ( for i, j being Element of P holds
( the Arrows of C . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of C . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ) from ORDERS_3:sch_1(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict AltCatStr st the carrier of b1 = P & ( for i, j being Element of P holds
( the Arrows of b1 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b1 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) & the carrier of b2 = P & ( for i, j being Element of P holds
( the Arrows of b2 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b2 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) holds
b1 = b2
proof
thus  for C1, C2 being strict AltCatStr st the carrier of C1 = P & ( for i, j being Element of P holds
( the Arrows of C1 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of C1 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) & the carrier of C2 = P & ( for i, j being Element of P holds
( the Arrows of C2 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of C2 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) holds
C1 = C2 from ORDERS_3:sch_2(); ::_thesis: verum
end;
end;

:: deftheorem Def9 defines POSAltCat ORDERS_3:def_9_:_
 for P being non empty POSet_set
for b2 being strict AltCatStr holds
( b2 = POSAltCat P iff ( the carrier of b2 = P & ( for i, j being Element of P holds
( the Arrows of b2 . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b2 . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ) );

registration
let P be non empty POSet_set;
cluster POSAltCat P ->  non empty transitive strict ;
coherence
 ( POSAltCat P is transitive & not POSAltCat P is empty )
proof
set A = POSAltCat P;
thus  POSAltCat P is transitive ::_thesis: not POSAltCat P is empty
proof
let o1, o2, o3 be object of (POSAltCat P); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider o19 = o1, o29 = o2, o39 = o3 as Element of P by Def9;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {}
 MonFuncs (o19,o29) <> {} by A1, Def9;
then consider f being set  such that
A3: f in MonFuncs (o19,o29) by XBOOLE_0:def_1;
 MonFuncs (o29,o39) <> {} by A2, Def9;
then consider g being set  such that
A4: g in MonFuncs (o29,o39) by XBOOLE_0:def_1;
reconsider f = f, g = g as Function by A3, A4;
 g * f in MonFuncs (o19,o39) by A3, A4, Th6;
hence  not <^o1,o3^> = {} by Def9; ::_thesis: verum
end;
thus  not POSAltCat P is empty by Def9; ::_thesis: verum
end;
end;

registration
let P be non empty POSet_set;
cluster POSAltCat P ->  strict associative with_units ;
coherence
 ( POSAltCat P is associative & POSAltCat P is with_units )
proof
set A = POSAltCat P;
set G = the Arrows of (POSAltCat P);
set C = the Comp of (POSAltCat P);
thus  the Comp of (POSAltCat P) is associative :: according to ALTCAT_1:def_15 ::_thesis: POSAltCat P is with_units
proof
let i, j, k, l be Element of (POSAltCat P); :: according to ALTCAT_1:def_5 ::_thesis: for b1, b2, b3 being set holds
( not b1 in the Arrows of (POSAltCat P) . (i,j) or not b2 in the Arrows of (POSAltCat P) . (j,k) or not b3 in the Arrows of (POSAltCat P) . (k,l) or ( the Comp of (POSAltCat P) . (i,k,l)) . (b3,(( the Comp of (POSAltCat P) . (i,j,k)) . (b2,b1))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (b3,b2)),b1) )
let f, g, h be set ; ::_thesis: ( not f in the Arrows of (POSAltCat P) . (i,j) or not g in the Arrows of (POSAltCat P) . (j,k) or not h in the Arrows of (POSAltCat P) . (k,l) or ( the Comp of (POSAltCat P) . (i,k,l)) . (h,(( the Comp of (POSAltCat P) . (i,j,k)) . (g,f))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (h,g)),f) )
reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of P by Def9;
assume that
A1: f in the Arrows of (POSAltCat P) . (i,j) and
A2: g in the Arrows of (POSAltCat P) . (j,k) and
A3: h in the Arrows of (POSAltCat P) . (k,l) ; ::_thesis: ( the Comp of (POSAltCat P) . (i,k,l)) . (h,(( the Comp of (POSAltCat P) . (i,j,k)) . (g,f))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (h,g)),f)
A4: g in MonFuncs (j9,k9) by A2, Def9;
A5: h in MonFuncs (k9,l9) by A3, Def9;
A6: f in MonFuncs (i9,j9) by A1, Def9;
then reconsider f9 = f, g9 = g, h9 = h as Function by A4, A5;
A7: the Comp of (POSAltCat P) . (i,j,l) = FuncComp ((MonFuncs (i9,j9)),(MonFuncs (j9,l9))) by Def9;
 the Comp of (POSAltCat P) . (j,k,l) = FuncComp ((MonFuncs (j9,k9)),(MonFuncs (k9,l9))) by Def9;
then A8: ( the Comp of (POSAltCat P) . (j,k,l)) . (h,g) = h9 * g9 by A4, A5, ALTCAT_1:11;
 the Comp of (POSAltCat P) . (i,j,k) = FuncComp ((MonFuncs (i9,j9)),(MonFuncs (j9,k9))) by Def9;
then A9: ( the Comp of (POSAltCat P) . (i,j,k)) . (g,f) = g9 * f9 by A6, A4, ALTCAT_1:11;
 h9 * g9 in MonFuncs (j9,l9) by A4, A5, Th6;
then A10: ( the Comp of (POSAltCat P) . (i,j,l)) . ((h9 * g9),f9) = (h9 * g9) * f9 by A6, A7, ALTCAT_1:11;
A11: the Comp of (POSAltCat P) . (i,k,l) = FuncComp ((MonFuncs (i9,k9)),(MonFuncs (k9,l9))) by Def9;
 g9 * f9 in MonFuncs (i9,k9) by A6, A4, Th6;
then  ( the Comp of (POSAltCat P) . (i,k,l)) . (h,(g9 * f9)) = h9 * (g9 * f9) by A5, A11, ALTCAT_1:11;
hence  ( the Comp of (POSAltCat P) . (i,k,l)) . (h,(( the Comp of (POSAltCat P) . (i,j,k)) . (g,f))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (h,g)),f) by A9, A8, A10, RELAT_1:36; ::_thesis: verum
end;
thus  the Comp of (POSAltCat P) is with_left_units :: according to ALTCAT_1:def_16 ::_thesis: the Comp of (POSAltCat P) is with_right_units
proof
let j be Element of (POSAltCat P); :: according to ALTCAT_1:def_7 ::_thesis: ex b1 being set st
( b1 in the Arrows of (POSAltCat P) . (j,j) & ( for b2 being Element of the carrier of (POSAltCat P)
for b3 being set holds
( not b3 in the Arrows of (POSAltCat P) . (b2,j) or ( the Comp of (POSAltCat P) . (b2,j,j)) . (b1,b3) = b3 ) ) )
reconsider j9 = j as Element of P by Def9;
take e = id the carrier of j9; ::_thesis: ( e in the Arrows of (POSAltCat P) . (j,j) & ( for b1 being Element of the carrier of (POSAltCat P)
for b2 being set holds
( not b2 in the Arrows of (POSAltCat P) . (b1,j) or ( the Comp of (POSAltCat P) . (b1,j,j)) . (e,b2) = b2 ) ) )
 the Arrows of (POSAltCat P) . (j,j) = MonFuncs (j9,j9) by Def9;
hence  e in the Arrows of (POSAltCat P) . (j,j) by Th7; ::_thesis: for b1 being Element of the carrier of (POSAltCat P)
for b2 being set holds
( not b2 in the Arrows of (POSAltCat P) . (b1,j) or ( the Comp of (POSAltCat P) . (b1,j,j)) . (e,b2) = b2 )
let i be Element of (POSAltCat P); ::_thesis: for b1 being set holds
( not b1 in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,j,j)) . (e,b1) = b1 )
let f be set ; ::_thesis: ( not f in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,j,j)) . (e,f) = f )
reconsider i9 = i as Element of P by Def9;
A12: the Comp of (POSAltCat P) . (i,j,j) = FuncComp ((MonFuncs (i9,j9)),(MonFuncs (j9,j9))) by Def9;
assume  f in the Arrows of (POSAltCat P) . (i,j) ; ::_thesis: ( the Comp of (POSAltCat P) . (i,j,j)) . (e,f) = f
then A13: f in MonFuncs (i9,j9) by Def9;
then consider f9 being Function of i9,j9 such that
A14: f = f9 and
 f9 in Funcs ( the carrier of i9, the carrier of j9) and
 f9 is monotone by Def6;
A15: e in MonFuncs (j9,j9) by Th7;
then consider e9 being Function of j9,j9 such that
A16: e = e9 and
 e9 in Funcs ( the carrier of j9, the carrier of j9) and
 e9 is monotone by Def6;
 rng f9 c= the carrier of j9 ;
then  e9 * f9 = f by A16, A14, RELAT_1:53;
hence  ( the Comp of (POSAltCat P) . (i,j,j)) . (e,f) = f by A15, A16, A13, A14, A12, ALTCAT_1:11; ::_thesis: verum
end;
thus  the Comp of (POSAltCat P) is with_right_units ::_thesis: verum
proof
let i be Element of (POSAltCat P); :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st
( b1 in the Arrows of (POSAltCat P) . (i,i) & ( for b2 being Element of the carrier of (POSAltCat P)
for b3 being set holds
( not b3 in the Arrows of (POSAltCat P) . (i,b2) or ( the Comp of (POSAltCat P) . (i,i,b2)) . (b3,b1) = b3 ) ) )
reconsider i9 = i as Element of P by Def9;
take e = id the carrier of i9; ::_thesis: ( e in the Arrows of (POSAltCat P) . (i,i) & ( for b1 being Element of the carrier of (POSAltCat P)
for b2 being set holds
( not b2 in the Arrows of (POSAltCat P) . (i,b1) or ( the Comp of (POSAltCat P) . (i,i,b1)) . (b2,e) = b2 ) ) )
 the Arrows of (POSAltCat P) . (i,i) = MonFuncs (i9,i9) by Def9;
hence  e in the Arrows of (POSAltCat P) . (i,i) by Th7; ::_thesis: for b1 being Element of the carrier of (POSAltCat P)
for b2 being set holds
( not b2 in the Arrows of (POSAltCat P) . (i,b1) or ( the Comp of (POSAltCat P) . (i,i,b1)) . (b2,e) = b2 )
let j be Element of (POSAltCat P); ::_thesis: for b1 being set holds
( not b1 in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,i,j)) . (b1,e) = b1 )
let f be set ; ::_thesis: ( not f in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,i,j)) . (f,e) = f )
reconsider j9 = j as Element of P by Def9;
A17: the Comp of (POSAltCat P) . (i,i,j) = FuncComp ((MonFuncs (i9,i9)),(MonFuncs (i9,j9))) by Def9;
assume  f in the Arrows of (POSAltCat P) . (i,j) ; ::_thesis: ( the Comp of (POSAltCat P) . (i,i,j)) . (f,e) = f
then A18: f in MonFuncs (i9,j9) by Def9;
then consider f9 being Function of i9,j9 such that
A19: f = f9 and
 f9 in Funcs ( the carrier of i9, the carrier of j9) and
 f9 is monotone by Def6;
A20: e in MonFuncs (i9,i9) by Th7;
then consider e9 being Function of i9,i9 such that
A21: e = e9 and
 e9 in Funcs ( the carrier of i9, the carrier of i9) and
 e9 is monotone by Def6;
 dom f9 = the carrier of i9 by FUNCT_2:def_1;
then  f9 * e9 = f by A21, A19, RELAT_1:52;
hence  ( the Comp of (POSAltCat P) . (i,i,j)) . (f,e) = f by A20, A21, A18, A19, A17, ALTCAT_1:11; ::_thesis: verum
end;
end;
end;

theorem :: ORDERS_3:12
for P being non empty POSet_set
for o1, o2 being object of (POSAltCat P)
for A, B being Element of P st o1 = A & o2 = B holds
<^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)
proof
let P be non empty POSet_set; ::_thesis: for o1, o2 being object of (POSAltCat P)
for A, B being Element of P st o1 = A & o2 = B holds
<^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)
let o1, o2 be object of (POSAltCat P); ::_thesis: for A, B being Element of P st o1 = A & o2 = B holds
<^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)
let A, B be Element of P; ::_thesis: ( o1 = A & o2 = B implies <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B) )
assume A1: ( o1 = A & o2 = B ) ; ::_thesis: <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <^o1,o2^> or x in Funcs ( the carrier of A, the carrier of B) )
assume  x in <^o1,o2^> ; ::_thesis: x in Funcs ( the carrier of A, the carrier of B)
then  x in MonFuncs (A,B) by A1, Def9;
then  ex f being Function of A,B st
( f = x & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by Def6;
hence  x in Funcs ( the carrier of A, the carrier of B) ; ::_thesis: verum
end;