:: YELLOW21 semantic presentation

definition
let c1 be set ;
func c1 as_1-sorted -> 1-sorted equals :Def1: :: YELLOW21:def 1
a1 if a1 is 1-sorted
otherwise 1-sorted(# a1 #);
coherence
( ( c1 is 1-sorted implies c1 is 1-sorted ) & ( c1 is not 1-sorted implies 1-sorted(# c1 #) is 1-sorted ) ) ;
consistency
for b1 being 1-sorted holds verum ;
end;

:: deftheorem Def1 defines as_1-sorted YELLOW21:def 1 :
for b1 being set holds
( ( b1 is 1-sorted implies b1 as_1-sorted = b1 ) & ( b1 is not 1-sorted implies b1 as_1-sorted = 1-sorted(# b1 #) ) );

definition
let c1 be set ;
defpred S1[ set ] means ( a1 is strict Poset & the carrier of (a1 as_1-sorted ) in c1 );
func POSETS c1 -> set means :Def2: :: YELLOW21:def 2
for b1 being set holds
( b1 in a2 iff ( b1 is strict Poset & the carrier of (b1 as_1-sorted ) in a1 ) );
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ( b3 is strict Poset & the carrier of (b3 as_1-sorted ) in c1 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 is strict Poset & the carrier of (b3 as_1-sorted ) in c1 ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 is strict Poset & the carrier of (b2 as_1-sorted ) in c1 ) )
proof end;
end;

:: deftheorem Def2 defines POSETS YELLOW21:def 2 :
for b1 being set
for b2 being set holds
( b2 = POSETS b1 iff for b3 being set holds
( b3 in b2 iff ( b3 is strict Poset & the carrier of (b3 as_1-sorted ) in b1 ) ) );

registration
let c1 be non empty set ;
cluster POSETS a1 -> non empty ;
coherence
not POSETS c1 is empty
proof end;
end;

registration
let c1 be with_non-empty_elements set ;
cluster POSETS a1 -> POSet_set-like ;
coherence
POSETS c1 is POSet_set-like
proof end;
end;

definition
let c1 be category;
attr a1 is carrier-underlaid means :Def3: :: YELLOW21:def 3
for b1 being object of a1 ex b2 being 1-sorted st
( b1 = b2 & the_carrier_of b1 = the carrier of b2 );
end;

:: deftheorem Def3 defines carrier-underlaid YELLOW21:def 3 :
for b1 being category holds
( b1 is carrier-underlaid iff for b2 being object of b1 ex b3 being 1-sorted st
( b2 = b3 & the_carrier_of b2 = the carrier of b3 ) );

definition
let c1 be category;
attr a1 is lattice-wise means :Def4: :: YELLOW21:def 4
( a1 is semi-functional & a1 is set-id-inheriting & ( for b1 being object of a1 holds b1 is LATTICE ) & ( for b1, b2 being object of a1
for b3, b4 being LATTICE st b3 = b1 & b4 = b2 holds
<^b1,b2^> c= MonFuncs b3,b4 ) );
end;

:: deftheorem Def4 defines lattice-wise YELLOW21:def 4 :
for b1 being category holds
( b1 is lattice-wise iff ( b1 is semi-functional & b1 is set-id-inheriting & ( for b2 being object of b1 holds b2 is LATTICE ) & ( for b2, b3 being object of b1
for b4, b5 being LATTICE st b4 = b2 & b5 = b3 holds
<^b2,b3^> c= MonFuncs b4,b5 ) ) );

definition
let c1 be category;
attr a1 is with_complete_lattices means :Def5: :: YELLOW21:def 5
( a1 is lattice-wise & ( for b1 being object of a1 holds b1 is complete LATTICE ) );
end;

:: deftheorem Def5 defines with_complete_lattices YELLOW21:def 5 :
for b1 being category holds
( b1 is with_complete_lattices iff ( b1 is lattice-wise & ( for b2 being object of b1 holds b2 is complete LATTICE ) ) );

registration
cluster with_complete_lattices -> lattice-wise AltCatStr ;
coherence
for b1 being category st b1 is with_complete_lattices holds
b1 is lattice-wise by Def5;
cluster lattice-wise -> concrete carrier-underlaid AltCatStr ;
coherence
for b1 being category st b1 is lattice-wise holds
( b1 is concrete & b1 is carrier-underlaid )
proof end;
end;

scheme :: YELLOW21:sch 1
s1{ F1() -> non empty set , P1[ set , set , set ] } :
ex b1 being strict category st
( b1 is lattice-wise & the carrier of b1 = F1() & ( for b2, b3 being LATTICE
for b4 being monotone Function of b2,b3 holds
( b4 in the Arrows of b1 . b2,b3 iff ( b2 in F1() & b3 in F1() & P1[b2,b3,b4] ) ) ) )
provided
E6: for b1 being Element of F1() holds b1 is LATTICE and
E7: for b1, b2, b3 being LATTICE st b1 in F1() & b2 in F1() & b3 in F1() holds
for b4 being Function of b1,b2
for b5 being Function of b2,b3 st P1[b1,b2,b4] & P1[b2,b3,b5] holds
P1[b1,b3,b5 * b4] and
E8: for b1 being LATTICE st b1 in F1() holds
P1[b1,b1, id b1]
proof end;

registration
cluster strict concrete carrier-underlaid lattice-wise with_complete_lattices AltCatStr ;
existence
ex b1 being category st
( b1 is strict & b1 is with_complete_lattices )
proof end;
end;

theorem Th1: :: YELLOW21:1
for b1 being carrier-underlaid category
for b2 being object of b1 holds the_carrier_of b2 = the carrier of (b2 as_1-sorted )
proof end;

theorem Th2: :: YELLOW21:2
for b1 being set-id-inheriting carrier-underlaid category
for b2 being object of b1 holds idm b2 = id (b2 as_1-sorted )
proof end;

notation
let c1 be lattice-wise category;
let c2 be object of c1;
synonym latt c2 for c1 as_1-sorted ;
end;

definition
let c1 be lattice-wise category;
let c2 be object of c1;
redefine func as_1-sorted as latt c2 -> LATTICE equals :: YELLOW21:def 6
a2;
coherence
c2 as_1-sorted is LATTICE
proof end;
compatibility
for b1 being LATTICE holds
( b1 = c2 as_1-sorted iff b1 = c2 )
proof end;
end;

:: deftheorem Def6 defines latt YELLOW21:def 6 :
for b1 being lattice-wise category
for b2 being object of b1 holds latt b2 = b2;

notation
let c1 be with_complete_lattices category;
let c2 be object of c1;
synonym latt c2 for c1 as_1-sorted ;
end;

definition
let c1 be with_complete_lattices category;
let c2 be object of c1;
redefine func as_1-sorted as latt c2 -> complete LATTICE;
coherence
c2 as_1-sorted is complete LATTICE by Def5;
end;

definition
let c1 be lattice-wise category;
let c2, c3 be object of c1;
assume E7: <^c2,c3^> <> {} ;
let c4 be Morphism of c2,c3;
func @ c4 -> monotone Function of (latt a2),(latt a3) equals :Def7: :: YELLOW21:def 7
a4;
coherence
c4 is monotone Function of (latt c2),(latt c3)
proof end;
end;

:: deftheorem Def7 defines @ YELLOW21:def 7 :
for b1 being lattice-wise category
for b2, b3 being object of b1 st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds @ b4 = b4;

theorem Th3: :: YELLOW21:3
for b1 being lattice-wise category
for b2, b3, b4 being object of b1 st <^b2,b3^> <> {} & <^b3,b4^> <> {} holds
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 holds b6 * b5 = (@ b6) * (@ b5)
proof end;

scheme :: YELLOW21:sch 2
s2{ F1() -> non empty set , P1[ set , set , set ] } :
ex b1 being strict lattice-wise category st
( the carrier of b1 = F1() & ( for b2, b3 being object of b1
for b4 being monotone Function of (latt b2),(latt b3) holds
( b4 in <^b2,b3^> iff P1[ latt b2, latt b3,b4] ) ) )
provided
E9: for b1 being Element of F1() holds b1 is LATTICE and
E10: for b1, b2, b3 being LATTICE st b1 in F1() & b2 in F1() & b3 in F1() holds
for b4 being Function of b1,b2
for b5 being Function of b2,b3 st P1[b1,b2,b4] & P1[b2,b3,b5] holds
P1[b1,b3,b5 * b4] and
E11: for b1 being LATTICE st b1 in F1() holds
P1[b1,b1, id b1]
proof end;

scheme :: YELLOW21:sch 3
s3{ F1() -> non empty set , P1[ set ], P2[ set , set , set ] } :
ex b1 being strict lattice-wise category st
( ( for b2 being LATTICE holds
( b2 is object of b1 iff ( b2 is strict & P1[b2] & the carrier of b2 in F1() ) ) ) & ( for b2, b3 being object of b1
for b4 being monotone Function of (latt b2),(latt b3) holds
( b4 in <^b2,b3^> iff P2[ latt b2, latt b3,b4] ) ) )
provided
E9: ex b1 being strict LATTICE st
( P1[b1] & the carrier of b1 in F1() ) and
E10: for b1, b2, b3 being LATTICE st P1[b1] & P1[b2] & P1[b3] holds
for b4 being Function of b1,b2
for b5 being Function of b2,b3 st P2[b1,b2,b4] & P2[b2,b3,b5] holds
P2[b1,b3,b5 * b4] and
E11: for b1 being LATTICE st P1[b1] holds
P2[b1,b1, id b1]
proof end;

scheme :: YELLOW21:sch 4
s4{ F1() -> non empty set , P1[ set , set , set ] } :
for b1, b2 being lattice-wise category st the carrier of b1 = F1() & ( for b3, b4 being object of b1
for b5 being monotone Function of (latt b3),(latt b4) holds
( b5 in <^b3,b4^> iff P1[b3,b4,b5] ) ) & the carrier of b2 = F1() & ( for b3, b4 being object of b2
for b5 being monotone Function of (latt b3),(latt b4) holds
( b5 in <^b3,b4^> iff P1[b3,b4,b5] ) ) holds
AltCatStr(# the carrier of b1,the Arrows of b1,the Comp of b1 #) = AltCatStr(# the carrier of b2,the Arrows of b2,the Comp of b2 #)
proof end;

scheme :: YELLOW21:sch 5
s5{ F1() -> non empty set , P1[ set ], P2[ set , set , set ] } :
for b1, b2 being lattice-wise category st ( for b3 being LATTICE holds
( b3 is object of b1 iff ( b3 is strict & P1[b3] & the carrier of b3 in F1() ) ) ) & ( for b3, b4 being object of b1
for b5 being monotone Function of (latt b3),(latt b4) holds
( b5 in <^b3,b4^> iff P2[b3,b4,b5] ) ) & ( for b3 being LATTICE holds
( b3 is object of b2 iff ( b3 is strict & P1[b3] & the carrier of b3 in F1() ) ) ) & ( for b3, b4 being object of b2
for b5 being monotone Function of (latt b3),(latt b4) holds
( b5 in <^b3,b4^> iff P2[b3,b4,b5] ) ) holds
AltCatStr(# the carrier of b1,the Arrows of b1,the Comp of b1 #) = AltCatStr(# the carrier of b2,the Arrows of b2,the Comp of b2 #)
proof end;

scheme :: YELLOW21:sch 6
s6{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } :
ex b1 being strict covariant Functor of F1(),F2() st
( ( for b2 being object of F1() holds b1 . b2 = F3((latt b2)) ) & ( for b2, b3 being object of F1() st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds b1 . b4 = F4((latt b2),(latt b3),(@ b4)) ) )
provided
E9: for b1, b2 being LATTICE
for b3 being Function of b1,b2 holds
( b3 in the Arrows of F1() . b1,b2 iff ( b1 in the carrier of F1() & b2 in the carrier of F1() & P1[b1,b2,b3] ) ) and
E10: for b1, b2 being LATTICE
for b3 being Function of b1,b2 holds
( b3 in the Arrows of F2() . b1,b2 iff ( b1 in the carrier of F2() & b2 in the carrier of F2() & P2[b1,b2,b3] ) ) and
E11: for b1 being LATTICE st b1 in the carrier of F1() holds
F3(b1) in the carrier of F2() and
E12: for b1, b2 being LATTICE
for b3 being Function of b1,b2 st P1[b1,b2,b3] holds
( F4(b1,b2,b3) is Function of F3(b1),F3(b2) & P2[F3(b1),F3(b2),F4(b1,b2,b3)] ) and
E13: for b1 being LATTICE st b1 in the carrier of F1() holds
F4(b1,b1,(id b1)) = id F3(b1) and
E14: for b1, b2, b3 being LATTICE
for b4 being Function of b1,b2
for b5 being Function of b2,b3 st P1[b1,b2,b4] & P1[b2,b3,b5] holds
F4(b1,b3,(b5 * b4)) = F4(b2,b3,b5) * F4(b1,b2,b4)
proof end;

scheme :: YELLOW21:sch 7
s7{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } :
ex b1 being strict contravariant Functor of F1(),F2() st
( ( for b2 being object of F1() holds b1 . b2 = F3((latt b2)) ) & ( for b2, b3 being object of F1() st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds b1 . b4 = F4((latt b2),(latt b3),(@ b4)) ) )
provided
E9: for b1, b2 being LATTICE
for b3 being Function of b1,b2 holds
( b3 in the Arrows of F1() . b1,b2 iff ( b1 in the carrier of F1() & b2 in the carrier of F1() & P1[b1,b2,b3] ) ) and
E10: for b1, b2 being LATTICE
for b3 being Function of b1,b2 holds
( b3 in the Arrows of F2() . b1,b2 iff ( b1 in the carrier of F2() & b2 in the carrier of F2() & P2[b1,b2,b3] ) ) and
E11: for b1 being LATTICE st b1 in the carrier of F1() holds
F3(b1) in the carrier of F2() and
E12: for b1, b2 being LATTICE
for b3 being Function of b1,b2 st P1[b1,b2,b3] holds
( F4(b1,b2,b3) is Function of F3(b2),F3(b1) & P2[F3(b2),F3(b1),F4(b1,b2,b3)] ) and
E13: for b1 being LATTICE st b1 in the carrier of F1() holds
F4(b1,b1,(id b1)) = id F3(b1) and
E14: for b1, b2, b3 being LATTICE
for b4 being Function of b1,b2
for b5 being Function of b2,b3 st P1[b1,b2,b4] & P1[b2,b3,b5] holds
F4(b1,b3,(b5 * b4)) = F4(b1,b2,b4) * F4(b2,b3,b5)
proof end;

scheme :: YELLOW21:sch 8
s8{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } :
F1(),F2() are_isomorphic
provided
E9: for b1, b2 being LATTICE
for b3 being Function of b1,b2 holds
( b3 in the Arrows of F1() . b1,b2 iff ( b1 in the carrier of F1() & b2 in the carrier of F1() & P1[b1,b2,b3] ) ) and
E10: for b1, b2 being LATTICE
for b3 being Function of b1,b2 holds
( b3 in the Arrows of F2() . b1,b2 iff ( b1 in the carrier of F2() & b2 in the carrier of F2() & P2[b1,b2,b3] ) ) and
E11: ex b1 being covariant Functor of F1(),F2() st
( ( for b2 being object of F1() holds b1 . b2 = F3(b2) ) & ( for b2, b3 being object of F1() st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds b1 . b4 = F4(b2,b3,b4) ) ) and
E12: for b1, b2 being LATTICE st b1 in the carrier of F1() & b2 in the carrier of F1() & F3(b1) = F3(b2) holds
b1 = b2 and
E13: for b1, b2 being LATTICE
for b3, b4 being Function of b1,b2 st P1[b1,b2,b3] & P1[b1,b2,b4] & F4(b1,b2,b3) = F4(b1,b2,b4) holds
b3 = b4 and
E14: for b1, b2 being LATTICE
for b3 being Function of b1,b2 st P2[b1,b2,b3] holds
ex b4, b5 being LATTICEex b6 being Function of b4,b5 st
( b4 in the carrier of F1() & b5 in the carrier of F1() & P1[b4,b5,b6] & b1 = F3(b4) & b2 = F3(b5) & b3 = F4(b4,b5,b6) )
proof end;

scheme :: YELLOW21:sch 9
s9{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set , set , set ) -> Function } :
F1(),F2() are_anti-isomorphic
provided
E9: for b1, b2 being LATTICE
for b3 being Function of b1,b2 holds
( b3 in the Arrows of F1() . b1,b2 iff ( b1 in the carrier of F1() & b2 in the carrier of F1() & P1[b1,b2,b3] ) ) and
E10: for b1, b2 being LATTICE
for b3 being Function of b1,b2 holds
( b3 in the Arrows of F2() . b1,b2 iff ( b1 in the carrier of F2() & b2 in the carrier of F2() & P2[b1,b2,b3] ) ) and
E11: ex b1 being contravariant Functor of F1(),F2() st
( ( for b2 being object of F1() holds b1 . b2 = F3(b2) ) & ( for b2, b3 being object of F1() st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds b1 . b4 = F4(b2,b3,b4) ) ) and
E12: for b1, b2 being LATTICE st b1 in the carrier of F1() & b2 in the carrier of F1() & F3(b1) = F3(b2) holds
b1 = b2 and
E13: for b1, b2 being LATTICE
for b3, b4 being Function of b1,b2 st F4(b1,b2,b3) = F4(b1,b2,b4) holds
b3 = b4 and
E14: for b1, b2 being LATTICE
for b3 being Function of b1,b2 st P2[b1,b2,b3] holds
ex b4, b5 being LATTICEex b6 being Function of b4,b5 st
( b4 in the carrier of F1() & b5 in the carrier of F1() & P1[b4,b5,b6] & b2 = F3(b4) & b1 = F3(b5) & b3 = F4(b4,b5,b6) )
proof end;

definition
let c1 be lattice-wise category;
attr a1 is with_all_isomorphisms means :Def8: :: YELLOW21:def 8
for b1, b2 being object of a1
for b3 being Function of (latt b1),(latt b2) st b3 is isomorphic holds
b3 in <^b1,b2^>;
end;

:: deftheorem Def8 defines with_all_isomorphisms YELLOW21:def 8 :
for b1 being lattice-wise category holds
( b1 is with_all_isomorphisms iff for b2, b3 being object of b1
for b4 being Function of (latt b2),(latt b3) st b4 is isomorphic holds
b4 in <^b2,b3^> );

registration
cluster strict concrete carrier-underlaid lattice-wise with_all_isomorphisms AltCatStr ;
existence
ex b1 being strict lattice-wise category st b1 is with_all_isomorphisms
proof end;
end;

theorem Th4: :: YELLOW21:4
for b1 being lattice-wise with_all_isomorphisms category
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 st @ b4 is isomorphic holds
b4 is iso
proof end;

theorem Th5: :: YELLOW21:5
for b1 being lattice-wise category
for b2, b3 being object of b1 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
for b4 being Morphism of b2,b3 st b4 is iso holds
@ b4 is isomorphic
proof end;

scheme :: YELLOW21:sch 10
s10{ P1[ set , set , set ], P2[ set , set , set ], F1() -> lattice-wise category, F2() -> lattice-wise category, F3( set ) -> LATTICE, F4( set ) -> LATTICE, F5( set , set , set ) -> Function, F6( set , set , set ) -> Function, F7( set ) -> Function, F8( set ) -> Function } :
F1(),F2() are_equivalent
provided
E10: for b1, b2 being object of F1()
for b3 being monotone Function of (latt b1),(latt b2) holds
( b3 in <^b1,b2^> iff P1[ latt b1, latt b2,b3] ) and
E11: for b1, b2 being object of F2()
for b3 being monotone Function of (latt b1),(latt b2) holds
( b3 in <^b1,b2^> iff P2[ latt b1, latt b2,b3] ) and
E12: ex b1 being covariant Functor of F1(),F2() st
( ( for b2 being object of F1() holds b1 . b2 = F3(b2) ) & ( for b2, b3 being object of F1() st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds b1 . b4 = F5(b2,b3,b4) ) ) and
E13: ex b1 being covariant Functor of F2(),F1() st
( ( for b2 being object of F2() holds b1 . b2 = F4(b2) ) & ( for b2, b3 being object of F2() st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds b1 . b4 = F6(b2,b3,b4) ) ) and
E14: for b1 being LATTICE st b1 in the carrier of F1() holds
ex b2 being monotone Function of F4(F3(b1)),b1 st
( b2 = F7(b1) & b2 is isomorphic & P1[F4(F3(b1)),b1,b2] & P1[b1,F4(F3(b1)),b2 " ] ) and
E15: for b1 being LATTICE st b1 in the carrier of F2() holds
ex b2 being monotone Function of b1,F3(F4(b1)) st
( b2 = F8(b1) & b2 is isomorphic & P2[b1,F3(F4(b1)),b2] & P2[F3(F4(b1)),b1,b2 " ] ) and
E16: for b1, b2 being object of F1() st <^b1,b2^> <> {} holds
for b3 being Morphism of b1,b2 holds F7(b2) * F6(F3(b1),F3(b2),F5(b1,b2,b3)) = (@ b3) * F7(b1) and
E17: for b1, b2 being object of F2() st <^b1,b2^> <> {} holds
for b3 being Morphism of b1,b2 holds F5(F4(b1),F4(b2),F6(b1,b2,b3)) * F8(b1) = F8(b2) * (@ b3)
proof end;

definition
let c1 be Relation;
attr a1 is upper-bounded means :Def9: :: YELLOW21:def 9
ex b1 being set st
for b2 being set st b2 in field a1 holds
[b2,b1] in a1;
end;

:: deftheorem Def9 defines upper-bounded YELLOW21:def 9 :
for b1 being Relation holds
( b1 is upper-bounded iff ex b2 being set st
for b3 being set st b3 in field b1 holds
[b3,b2] in b1 );

Lemma11: for b1, b2 being set holds
( b1 in b2 iff b2 = (b2 \ {b1}) \/ {b1} )
proof end;

registration
cluster well-ordering -> well_founded reflexive antisymmetric connected transitive set ;
coherence
for b1 being Relation st b1 is well-ordering holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded ) by WELLORD1:def 4;
end;

registration
cluster well_founded well-ordering reflexive antisymmetric connected transitive set ;
existence
ex b1 being Relation st b1 is well-ordering
proof end;
end;

theorem Th6: :: YELLOW21:6
for b1, b2 being set
for b3 being one-to-one Function
for b4 being Relation holds
( [b1,b2] in (b3 * b4) * (b3 " ) iff ( b1 in dom b3 & b2 in dom b3 & [(b3 . b1),(b3 . b2)] in b4 ) )
proof end;

registration
let c1 be one-to-one Function;
let c2 be reflexive Relation;
cluster (a1 * a2) * (a1 " ) -> reflexive ;
coherence
(c1 * c2) * (c1 " ) is reflexive
proof end;
end;

registration
let c1 be one-to-one Function;
let c2 be antisymmetric Relation;
cluster (a1 * a2) * (a1 " ) -> antisymmetric ;
coherence
(c1 * c2) * (c1 " ) is antisymmetric
proof end;
end;

registration
let c1 be one-to-one Function;
let c2 be transitive Relation;
cluster (a1 * a2) * (a1 " ) -> transitive ;
coherence
(c1 * c2) * (c1 " ) is transitive
proof end;
end;

theorem Th7: :: YELLOW21:7
for b1 being set
for b2 being Ordinal st b1,b2 are_equipotent holds
ex b3 being Order of b1 st
( b3 well_orders b1 & order_type_of b3 = b2 )
proof end;

registration
let c1 be non empty set ;
cluster well_founded well-ordering connected upper-bounded Relation of a1,a1;
existence
ex b1 being Order of c1 st
( b1 is upper-bounded & b1 is well-ordering )
proof end;
end;

theorem Th8: :: YELLOW21:8
for b1 being non empty reflexive RelStr holds
( b1 is upper-bounded iff the InternalRel of b1 is upper-bounded )
proof end;

theorem Th9: :: YELLOW21:9
for b1 being non empty upper-bounded Poset st the InternalRel of b1 is well-ordering holds
( b1 is connected & b1 is complete & b1 is continuous )
proof end;

theorem Th10: :: YELLOW21:10
for b1 being non empty upper-bounded Poset st the InternalRel of b1 is well-ordering holds
for b2, b3 being Element of b1 st b3 < b2 holds
ex b4 being Element of b1 st
( b4 is compact & b3 <= b4 & b4 <= b2 )
proof end;

theorem Th11: :: YELLOW21:11
for b1 being non empty upper-bounded Poset st the InternalRel of b1 is well-ordering holds
b1 is algebraic
proof end;

registration
let c1 be non empty set ;
let c2 be well-ordering upper-bounded Order of c1;
cluster RelStr(# a1,a2 #) -> connected algebraic complete continuous ;
coherence
( RelStr(# c1,c2 #) is complete & RelStr(# c1,c2 #) is connected & RelStr(# c1,c2 #) is continuous & RelStr(# c1,c2 #) is algebraic )
proof end;
end;

registration
cluster non trivial -> with_non-empty_element set ;
coherence
for b1 being set st not b1 is trivial holds
b1 is with_non-empty_element
proof end;
end;

definition
let c1 be non empty set ;
given c2 being Element of c1 such that E18: not c2 is empty ;
defpred S1[ LATTICE] means a1 is complete;
defpred S2[ LATTICE, LATTICE, Function of a1,a2] means a3 is directed-sups-preserving;
func c1 -UPS_category -> strict lattice-wise category means :Def10: :: YELLOW21:def 10
( ( for b1 being LATTICE holds
( b1 is object of a2 iff ( b1 is strict & b1 is complete & the carrier of b1 in a1 ) ) ) & ( for b1, b2 being object of a2
for b3 being monotone Function of (latt b1),(latt b2) holds
( b3 in <^b1,b2^> iff b3 is directed-sups-preserving ) ) );
existence
ex b1 being strict lattice-wise category st
( ( for b2 being LATTICE holds
( b2 is object of b1 iff ( b2 is strict & b2 is complete & the carrier of b2 in c1 ) ) ) & ( for b2, b3 being object of b1
for b4 being monotone Function of (latt b2),(latt b3) holds
( b4 in <^b2,b3^> iff b4 is directed-sups-preserving ) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict lattice-wise category st ( for b3 being LATTICE holds
( b3 is object of b1 iff ( b3 is strict & b3 is complete & the carrier of b3 in c1 ) ) ) & ( for b3, b4 being object of b1
for b5 being monotone Function of (latt b3),(latt b4) holds
( b5 in <^b3,b4^> iff b5 is directed-sups-preserving ) ) & ( for b3 being LATTICE holds
( b3 is object of b2 iff ( b3 is strict & b3 is complete & the carrier of b3 in c1 ) ) ) & ( for b3, b4 being object of b2
for b5 being monotone Function of (latt b3),(latt b4) holds
( b5 in <^b3,b4^> iff b5 is directed-sups-preserving ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def10 defines -UPS_category YELLOW21:def 10 :
for b1 being non empty set st not for b2 being Element of b1 holds b2 is empty holds
for b2 being strict lattice-wise category holds
( b2 = b1 -UPS_category iff ( ( for b3 being LATTICE holds
( b3 is object of b2 iff ( b3 is strict & b3 is complete & the carrier of b3 in b1 ) ) ) & ( for b3, b4 being object of b2
for b5 being monotone Function of (latt b3),(latt b4) holds
( b5 in <^b3,b4^> iff b5 is directed-sups-preserving ) ) ) );

registration
let c1 be with_non-empty_element set ;
cluster a1 -UPS_category -> strict concrete carrier-underlaid lattice-wise with_complete_lattices with_all_isomorphisms ;
coherence
( c1 -UPS_category is with_complete_lattices & c1 -UPS_category is with_all_isomorphisms )
proof end;
end;

theorem Th12: :: YELLOW21:12
for b1 being with_non-empty_element set holds the carrier of (b1 -UPS_category ) c= POSETS b1
proof end;

theorem Th13: :: YELLOW21:13
for b1 being with_non-empty_element set
for b2 being set holds
( b2 is object of (b1 -UPS_category ) iff ( b2 is complete LATTICE & b2 in POSETS b1 ) )
proof end;

theorem Th14: :: YELLOW21:14
for b1 being with_non-empty_element set
for b2 being LATTICE st the carrier of b2 in b1 holds
( b2 is object of (b1 -UPS_category ) iff ( b2 is strict & b2 is complete ) )
proof end;

theorem Th15: :: YELLOW21:15
for b1 being with_non-empty_element set
for b2, b3 being object of (b1 -UPS_category )
for b4 being set holds
( b4 in <^b2,b3^> iff b4 is directed-sups-preserving Function of (latt b2),(latt b3) )
proof end;

registration
let c1 be with_non-empty_element set ;
let c2, c3 be object of (c1 -UPS_category );
cluster <^a2,a3^> -> non empty ;
coherence
not <^c2,c3^> is empty
proof end;
end;

theorem Th16: :: YELLOW21:16
for b1 being category
for b2 being non empty subcategory of b1
for b3 being object of b1
for b4 being object of b2 st b4 = b3 holds
the_carrier_of b4 = the_carrier_of b3 by ALTCAT_2:35;

registration
let c1 be set-id-inheriting category;
cluster non empty -> non empty set-id-inheriting SubCatStr of a1;
coherence
for b1 being non empty subcategory of c1 holds b1 is set-id-inheriting
proof end;
end;

registration
let c1 be para-functional category;
cluster non empty -> non empty para-functional SubCatStr of a1;
coherence
for b1 being non empty subcategory of c1 holds b1 is para-functional
proof end;
end;

registration
let c1 be semi-functional category;
cluster non empty transitive -> non empty transitive semi-functional SubCatStr of a1;
coherence
for b1 being non empty transitive SubCatStr of c1 holds b1 is semi-functional
proof end;
end;

registration
let c1 be carrier-underlaid category;
cluster non empty -> non empty carrier-underlaid SubCatStr of a1;
coherence
for b1 being non empty subcategory of c1 holds b1 is carrier-underlaid
proof end;
end;

registration
let c1 be lattice-wise category;
cluster non empty -> non empty semi-functional para-functional set-id-inheriting concrete carrier-underlaid lattice-wise SubCatStr of a1;
coherence
for b1 being non empty subcategory of c1 holds b1 is lattice-wise
proof end;
end;

registration
let c1 be lattice-wise with_all_isomorphisms category;
cluster non empty full -> non empty semi-functional para-functional set-id-inheriting concrete carrier-underlaid lattice-wise with_all_isomorphisms SubCatStr of a1;
coherence
for b1 being non empty subcategory of c1 st b1 is full holds
b1 is with_all_isomorphisms
proof end;
end;

registration
let c1 be with_complete_lattices category;
cluster non empty -> non empty semi-functional para-functional set-id-inheriting concrete carrier-underlaid lattice-wise with_complete_lattices SubCatStr of a1;
coherence
for b1 being non empty subcategory of c1 holds b1 is with_complete_lattices
proof end;
end;

definition
let c1 be with_non-empty_element set ;
defpred S1[ object of (c1 -UPS_category )] means latt a1 is continuous;
consider c2 being non empty set such that
E24: c2 in c1 by SETFAM_1:def 11;
consider c3 being well-ordering upper-bounded Order of c2;
set c4 = RelStr(# c2,c3 #);
func c1 -CONT_category -> non empty strict full subcategory of a1 -UPS_category means :Def11: :: YELLOW21:def 11
for b1 being object of (a1 -UPS_category ) holds
( b1 is object of a2 iff latt b1 is continuous );
existence
ex b1 being non empty strict full subcategory of c1 -UPS_category st
for b2 being object of (c1 -UPS_category ) holds
( b2 is object of b1 iff latt b2 is continuous )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of c1 -UPS_category st ( for b3 being object of (c1 -UPS_category ) holds
( b3 is object of b1 iff latt b3 is continuous ) ) & ( for b3 being object of (c1 -UPS_category ) holds
( b3 is object of b2 iff latt b3 is continuous ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def11 defines -CONT_category YELLOW21:def 11 :
for b1 being with_non-empty_element set
for b2 being non empty strict full subcategory of b1 -UPS_category holds
( b2 = b1 -CONT_category iff for b3 being object of (b1 -UPS_category ) holds
( b3 is object of b2 iff latt b3 is continuous ) );

definition
let c1 be with_non-empty_element set ;
defpred S1[ object of (c1 -CONT_category )] means latt a1 is algebraic;
consider c2 being non empty set such that
E25: c2 in c1 by SETFAM_1:def 11;
consider c3 being well-ordering upper-bounded Order of c2;
set c4 = RelStr(# c2,c3 #);
func c1 -ALG_category -> non empty strict full subcategory of a1 -CONT_category means :Def12: :: YELLOW21:def 12
for b1 being object of (a1 -CONT_category ) holds
( b1 is object of a2 iff latt b1 is algebraic );
existence
ex b1 being non empty strict full subcategory of c1 -CONT_category st
for b2 being object of (c1 -CONT_category ) holds
( b2 is object of b1 iff latt b2 is algebraic )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of c1 -CONT_category st ( for b3 being object of (c1 -CONT_category ) holds
( b3 is object of b1 iff latt b3 is algebraic ) ) & ( for b3 being object of (c1 -CONT_category ) holds
( b3 is object of b2 iff latt b3 is algebraic ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def12 defines -ALG_category YELLOW21:def 12 :
for b1 being with_non-empty_element set
for b2 being non empty strict full subcategory of b1 -CONT_category holds
( b2 = b1 -ALG_category iff for b3 being object of (b1 -CONT_category ) holds
( b3 is object of b2 iff latt b3 is algebraic ) );

theorem Th17: :: YELLOW21:17
for b1 being with_non-empty_element set
for b2 being LATTICE st the carrier of b2 in b1 holds
( b2 is object of (b1 -CONT_category ) iff ( b2 is strict & b2 is complete & b2 is continuous ) )
proof end;

theorem Th18: :: YELLOW21:18
for b1 being with_non-empty_element set
for b2 being LATTICE st the carrier of b2 in b1 holds
( b2 is object of (b1 -ALG_category ) iff ( b2 is strict & b2 is complete & b2 is algebraic ) )
proof end;

theorem Th19: :: YELLOW21:19
for b1 being with_non-empty_element set
for b2, b3 being object of (b1 -CONT_category )
for b4 being set holds
( b4 in <^b2,b3^> iff b4 is directed-sups-preserving Function of (latt b2),(latt b3) )
proof end;

theorem Th20: :: YELLOW21:20
for b1 being with_non-empty_element set
for b2, b3 being object of (b1 -ALG_category )
for b4 being set holds
( b4 in <^b2,b3^> iff b4 is directed-sups-preserving Function of (latt b2),(latt b3) )
proof end;

registration
let c1 be with_non-empty_element set ;
let c2, c3 be object of (c1 -CONT_category );
cluster <^a2,a3^> -> non empty ;
coherence
not <^c2,c3^> is empty
proof end;
end;

registration
let c1 be with_non-empty_element set ;
let c2, c3 be object of (c1 -ALG_category );
cluster <^a2,a3^> -> non empty ;
coherence
not <^c2,c3^> is empty
proof end;
end;