:: YELLOW21 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

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

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

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

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

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

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

definition
let C be category;
attr C is lattice-wise means :Def4: :: YELLOW21:def 4
( C is semi-functional & C is set-id-inheriting & ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs A,B ) );
end;

:: deftheorem Def4 defines lattice-wise YELLOW21:def 4 :
for C being category holds
( C is lattice-wise iff ( C is semi-functional & C is set-id-inheriting & ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs A,B ) ) );

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

:: deftheorem Def5 defines with_complete_lattices YELLOW21:def 5 :
for C being category holds
( C is with_complete_lattices iff ( C is lattice-wise & ( for a being object of C holds a 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
localCLCatEx{ F1() -> non empty set , P1[ set , set , set ] } :
ex C being strict category st
( C is lattice-wise & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . a,b iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )
provided
A1: for a being Element of F1() holds a is LATTICE and
A2: for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
P1[a,c,g * f] and
A3: for a being LATTICE st a in F1() holds
P1[a,a, id a]
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 :: YELLOW21:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being carrier-underlaid category
for a being object of C holds the_carrier_of a = the carrier of (a as_1-sorted )
proof end;

theorem Th2: :: YELLOW21:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being set-id-inheriting carrier-underlaid category
for a being object of C holds idm a = id (a as_1-sorted )
proof end;

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

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

:: deftheorem defines latt YELLOW21:def 6 :
for C being lattice-wise category
for a being object of C holds latt a = a;

notation
let C be with_complete_lattices category;
let a be object of C;
synonym latt a for C as_1-sorted ;
end;

definition
let C be with_complete_lattices category;
let a be object of C;
:: original: as_1-sorted
redefine func latt a -> complete LATTICE;
coherence
a as_1-sorted is complete LATTICE by Def5;
end;

definition
let C be lattice-wise category;
let a, b be object of C;
assume A1: <^a,b^> <> {} ;
let f be Morphism of a,b;
func @ f -> monotone Function of (latt a),(latt b) equals :Def7: :: YELLOW21:def 7
f;
coherence
f is monotone Function of (latt a),(latt b)
proof end;
end;

:: deftheorem Def7 defines @ YELLOW21:def 7 :
for C being lattice-wise category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds @ f = f;

theorem Th3: :: YELLOW21:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being lattice-wise category
for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (@ g) * (@ f)
proof end;

scheme :: YELLOW21:sch 2
CLCatEx1{ F1() -> non empty set , P1[ set , set , set ] } :
ex C being strict lattice-wise category st
( the carrier of C = F1() & ( for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] ) ) )
provided
A1: for a being Element of F1() holds a is LATTICE and
A2: for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
P1[a,c,g * f] and
A3: for a being LATTICE st a in F1() holds
P1[a,a, id a]
proof end;

scheme :: YELLOW21:sch 3
CLCatEx2{ F1() -> non empty set , P1[ set ], P2[ set , set , set ] } :
ex C being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) ) )
provided
A1: ex x being strict LATTICE st
( P1[x] & the carrier of x in F1() ) and
A2: for a, b, c being LATTICE st P1[a] & P1[b] & P1[c] holds
for f being Function of a,b
for g being Function of b,c st P2[a,b,f] & P2[b,c,g] holds
P2[a,c,g * f] and
A3: for a being LATTICE st P1[a] holds
P2[a,a, id a]
proof end;

scheme :: YELLOW21:sch 4
CLCatUniq1{ F1() -> non empty set , P1[ set , set , set ] } :
for C1, C2 being lattice-wise category st the carrier of C1 = F1() & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) ) & the carrier of C2 = F1() & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) ) holds
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)
proof end;

scheme :: YELLOW21:sch 5
CLCatUniq2{ F1() -> non empty set , P1[ set ], P2[ set , set , set ] } :
for C1, C2 being lattice-wise category st ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) holds
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #)
proof end;

scheme :: YELLOW21:sch 6
CLCovariantFunctorEx{ 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 F being strict covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
provided
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F1() . a,b iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F2() . a,b iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and
A3: for a being LATTICE st a in the carrier of F1() holds
F3(a) in the carrier of F2() and
A4: for a, b being LATTICE
for f being Function of a,b st P1[a,b,f] holds
( F4(a,b,f) is Function of F3(a),F3(b) & P2[F3(a),F3(b),F4(a,b,f)] ) and
A5: for a being LATTICE st a in the carrier of F1() holds
F4(a,a,(id a)) = id F3(a) and
A6: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
F4(a,c,(g * f)) = F4(b,c,g) * F4(a,b,f)
proof end;

scheme :: YELLOW21:sch 7
CLContravariantFunctorEx{ 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 F being strict contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3((latt a)) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
provided
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F1() . a,b iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F2() . a,b iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and
A3: for a being LATTICE st a in the carrier of F1() holds
F3(a) in the carrier of F2() and
A4: for a, b being LATTICE
for f being Function of a,b st P1[a,b,f] holds
( F4(a,b,f) is Function of F3(b),F3(a) & P2[F3(b),F3(a),F4(a,b,f)] ) and
A5: for a being LATTICE st a in the carrier of F1() holds
F4(a,a,(id a)) = id F3(a) and
A6: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
F4(a,c,(g * f)) = F4(a,b,f) * F4(b,c,g)
proof end;

scheme :: YELLOW21:sch 8
CLCatIsomorphism{ 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
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F1() . a,b iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F2() . a,b iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and
A3: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and
A4: for a, b being LATTICE st a in the carrier of F1() & b in the carrier of F1() & F3(a) = F3(b) holds
a = b and
A5: for a, b being LATTICE
for f, g being Function of a,b st P1[a,b,f] & P1[a,b,g] & F4(a,b,f) = F4(a,b,g) holds
f = g and
A6: for a, b being LATTICE
for f being Function of a,b st P2[a,b,f] holds
ex c, d being LATTICE ex g being Function of c,d st
( c in the carrier of F1() & d in the carrier of F1() & P1[c,d,g] & a = F3(c) & b = F3(d) & f = F4(c,d,g) )
proof end;

scheme :: YELLOW21:sch 9
CLCatAntiIsomorphism{ 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
A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F1() . a,b iff ( a in the carrier of F1() & b in the carrier of F1() & P1[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F2() . a,b iff ( a in the carrier of F2() & b in the carrier of F2() & P2[a,b,f] ) ) and
A3: ex F being contravariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) ) and
A4: for a, b being LATTICE st a in the carrier of F1() & b in the carrier of F1() & F3(a) = F3(b) holds
a = b and
A5: for a, b being LATTICE
for f, g being Function of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g and
A6: for a, b being LATTICE
for f being Function of a,b st P2[a,b,f] holds
ex c, d being LATTICE ex g being Function of c,d st
( c in the carrier of F1() & d in the carrier of F1() & P1[c,d,g] & b = F3(c) & a = F3(d) & f = F4(c,d,g) )
proof end;

definition
let C be lattice-wise category;
attr C is with_all_isomorphisms means :Def8: :: YELLOW21:def 8
for a, b being object of C
for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^>;
end;

:: deftheorem Def8 defines with_all_isomorphisms YELLOW21:def 8 :
for C being lattice-wise category holds
( C is with_all_isomorphisms iff for a, b being object of C
for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^> );

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 :: YELLOW21:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being lattice-wise with_all_isomorphisms category
for a, b being object of C
for f being Morphism of a,b st @ f is isomorphic holds
f is iso
proof end;

theorem :: YELLOW21:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being lattice-wise category
for a, b being object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
@ f is isomorphic
proof end;

scheme :: YELLOW21:sch 10
CLCatEquivalence{ 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
A1: for a, b being object of F1()
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] ) and
A2: for a, b being object of F2()
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) and
A3: ex F being covariant Functor of F1(),F2() st
( ( for a being object of F1() holds F . a = F3(a) ) & ( for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F5(a,b,f) ) ) and
A4: ex G being covariant Functor of F2(),F1() st
( ( for a being object of F2() holds G . a = F4(a) ) & ( for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f) ) ) and
A5: for a being LATTICE st a in the carrier of F1() holds
ex f being monotone Function of F4(F3(a)),a st
( f = F7(a) & f is isomorphic & P1[F4(F3(a)),a,f] & P1[a,F4(F3(a)),f " ] ) and
A6: for a being LATTICE st a in the carrier of F2() holds
ex f being monotone Function of a,F3(F4(a)) st
( f = F8(a) & f is isomorphic & P2[a,F3(F4(a)),f] & P2[F3(F4(a)),a,f " ] ) and
A7: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = (@ f) * F7(a) and
A8: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * (@ f)
proof end;

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

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

Lm1: for x, X being set holds
( x in X iff X = (X \ {x}) \/ {x} )
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f being one-to-one Function
for R being Relation holds
( [x,y] in (f * R) * (f " ) iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )
proof end;

registration
let f be one-to-one Function;
let R be reflexive Relation;
cluster (f * R) * (f " ) -> reflexive ;
coherence
(f * R) * (f " ) is reflexive
proof end;
end;

registration
let f be one-to-one Function;
let R be antisymmetric Relation;
cluster (f * R) * (f " ) -> antisymmetric ;
coherence
(f * R) * (f " ) is antisymmetric
proof end;
end;

registration
let f be one-to-one Function;
let R be transitive Relation;
cluster (f * R) * (f " ) -> transitive ;
coherence
(f * R) * (f " ) is transitive
proof end;
end;

theorem Th7: :: YELLOW21:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal st X,A are_equipotent holds
ex R being Order of X st
( R well_orders X & order_type_of R = A )
proof end;

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

theorem Th8: :: YELLOW21:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty reflexive RelStr holds
( P is upper-bounded iff the InternalRel of P is upper-bounded )
proof end;

theorem Th9: :: YELLOW21:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
( P is connected & P is complete & P is continuous )
proof end;

theorem Th10: :: YELLOW21:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
for x, y being Element of P st y < x holds
ex z being Element of P st
( z is compact & y <= z & z <= x )
proof end;

theorem Th11: :: YELLOW21:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
P is algebraic
proof end;

registration
let X be non empty set ;
let R be well-ordering upper-bounded Order of X;
cluster RelStr(# X,R #) -> connected algebraic complete continuous ;
coherence
( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) 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 W be non empty set ;
given w being Element of W such that A1: not w is empty ;
defpred S1[ LATTICE] means $1 is complete;
defpred S2[ LATTICE, LATTICE, Function of $1,$2] means $3 is directed-sups-preserving;
func W -UPS_category -> strict lattice-wise category means :Def10: :: YELLOW21:def 10
( ( for x being LATTICE holds
( x is object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of it
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) );
existence
ex b1 being strict lattice-wise category st
( ( for x being LATTICE holds
( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds
( x is object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) & ( for x being LATTICE holds
( x is object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) holds
b1 = b2;
proof end;
end;

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

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

theorem Th12: :: YELLOW21:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being with_non-empty_element set holds the carrier of (W -UPS_category ) c= POSETS W
proof end;

theorem Th13: :: YELLOW21:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being with_non-empty_element set
for x being set holds
( x is object of (W -UPS_category ) iff ( x is complete LATTICE & x in POSETS W ) )
proof end;

theorem Th14: :: YELLOW21:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is object of (W -UPS_category ) iff ( L is strict & L is complete ) )
proof end;

theorem Th15: :: YELLOW21:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being with_non-empty_element set
for a, b being object of (W -UPS_category )
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof end;

registration
let W be with_non-empty_element set ;
let a, b be object of (W -UPS_category );
cluster <^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof end;
end;

theorem Th16: :: YELLOW21:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being category
for B being non empty subcategory of A
for a being object of A
for b being object of B st b = a holds
the_carrier_of b = the_carrier_of a by ALTCAT_2:35;

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

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

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

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

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

registration
let A 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 A;
coherence
for b1 being non empty subcategory of A st b1 is full holds
b1 is with_all_isomorphisms
proof end;
end;

registration
let A 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 A;
coherence
for b1 being non empty subcategory of A holds b1 is with_complete_lattices
proof end;
end;

definition
let W be with_non-empty_element set ;
defpred S1[ object of (W -UPS_category )] means latt $1 is continuous;
consider a being non empty set such that
A1: a in W by SETFAM_1:def 11;
consider r being well-ordering upper-bounded Order of a;
set b = RelStr(# a,r #);
func W -CONT_category -> non empty strict full subcategory of W -UPS_category means :Def11: :: YELLOW21:def 11
for a being object of (W -UPS_category ) holds
( a is object of it iff latt a is continuous );
existence
ex b1 being non empty strict full subcategory of W -UPS_category st
for a being object of (W -UPS_category ) holds
( a is object of b1 iff latt a is continuous )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -UPS_category st ( for a being object of (W -UPS_category ) holds
( a is object of b1 iff latt a is continuous ) ) & ( for a being object of (W -UPS_category ) holds
( a is object of b2 iff latt a is continuous ) ) holds
b1 = b2;
proof end;
end;

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

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

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

theorem Th17: :: YELLOW21:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is object of (W -CONT_category ) iff ( L is strict & L is complete & L is continuous ) )
proof end;

theorem :: YELLOW21:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is object of (W -ALG_category ) iff ( L is strict & L is complete & L is algebraic ) )
proof end;

theorem Th19: :: YELLOW21:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being with_non-empty_element set
for a, b being object of (W -CONT_category )
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof end;

theorem Th20: :: YELLOW21:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being with_non-empty_element set
for a, b being object of (W -ALG_category )
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof end;

registration
let W be with_non-empty_element set ;
let a, b be object of (W -CONT_category );
cluster <^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof end;
end;

registration
let W be with_non-empty_element set ;
let a, b be object of (W -ALG_category );
cluster <^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof end;
end;