scheme :: YELLOW21:sch 8
CLCatIsomorphism{ P₁[ set , set , set ], P₂[ set , set , set ], F₁() -> lattice-wise category, F₂() -> lattice-wise category, F₃( set ) -> LATTICE, F₄( set , set , set ) -> Function } :

F₁(),F₂() are_isomorphic

provided

A1: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F₁() . (a,b) iff ( a in the carrier of F₁() & b in the carrier of F₁() & P₁[a,b,f] ) ) and
A2: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of F₂() . (a,b) iff ( a in the carrier of F₂() & b in the carrier of F₂() & P₂[a,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: for a, b being LATTICE st a in the carrier of F₁() & b in the carrier of F₁() & F₃(a) = F₃(b) holds
a = b and
A5: for a, b being LATTICE
for f, g being Function of a,b st P₁[a,b,f] & P₁[a,b,g] & F₄(a,b,f) = F₄(a,b,g) holds
f = g and
A6: for a, b being LATTICE
for f being Function of a,b st P₂[a,b,f] holds
ex c, d being LATTICE ex g being Function of c,d st
( c in the carrier of F₁() & d in the carrier of F₁() & P₁[c,d,g] & a = F₃(c) & b = F₃(d) & f = F₄(c,d,g) )