ex F being strict contravariant Functor of F₁(),F₂() st
( ( for a being Object of F₁() holds F . a = F₃((latt a)) ) & ( for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F₄((latt a),(latt b),(@ f)) ) )

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: for a being LATTICE st a in the carrier of F₁() holds
F₃(a) in the carrier of F₂() and
A4: for a, b being LATTICE
for f being Function of a,b st P₁[a,b,f] holds
( F₄(a,b,f) is Function of F₃(b),F₃(a) & P₂[F₃(b),F₃(a),F₄(a,b,f)] ) and
A5: for a being LATTICE st a in the carrier of F₁() holds
F₄(a,a,(id a)) = id F₃(a) and
A6: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st P₁[a,b,f] & P₁[b,c,g] holds
F₄(a,c,(g * f)) = F₄(a,b,f) * F₄(b,c,g)