scheme :: YELLOW21:sch 10
CLCatEquivalence{ P₁[ set , set , set ], P₂[ set , set , set ], F₁() -> lattice-wise category, F₂() -> lattice-wise category, F₃( set ) -> LATTICE, F₄( set ) -> LATTICE, F₅( set , set , set ) -> Function, F₆( set , set , set ) -> Function, F₇( set ) -> Function, F₈( set ) -> Function } :

F₁(),F₂() are_equivalent

provided

A1: for a, b being Object of F₁()
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₁[ latt a, latt b,f] ) and
A2: for a, b being Object of F₂()
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₂[ latt a, latt b,f] ) and
A3: ex F being covariant Functor of F₁(),F₂() st
( ( for a being Object of F₁() holds F . a = F₃(a) ) & ( for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F₅(a,b,f) ) ) and
A4: ex G being covariant Functor of F₂(),F₁() st
( ( for a being Object of F₂() holds G . a = F₄(a) ) & ( for a, b being Object of F₂() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F₆(a,b,f) ) ) and
A5: for a being LATTICE st a in the carrier of F₁() holds
ex f being monotone Function of F₄(F₃(a)),a st
( f = F₇(a) & f is isomorphic & P₁[F₄(F₃(a)),a,f] & P₁[a,F₄(F₃(a)),f " ] ) and
A6: for a being LATTICE st a in the carrier of F₂() holds
ex f being monotone Function of a,F₃(F₄(a)) st
( f = F₈(a) & f is isomorphic & P₂[a,F₃(F₄(a)),f] & P₂[F₃(F₄(a)),a,f " ] ) and
A7: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F₇(b) * F₆(F₃(a),F₃(b),F₅(a,b,f)) = (@ f) * F₇(a) and
A8: for a, b being Object of F₂() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F₅(F₄(a),F₄(b),F₆(a,b,f)) * F₈(a) = F₈(b) * (@ f)