ex C being strict category st
( C is lattice-wise & the carrier of C = F₁() & ( 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 F₁() & b in F₁() & P₁[a,b,f] ) ) ) )

A1: for a being Element of F₁() holds a is LATTICE and
A2: for a, b, c being LATTICE st a in F₁() & b in F₁() & c in F₁() holds
for f being Function of a,b
for g being Function of b,c st P₁[a,b,f] & P₁[b,c,g] holds
P₁[a,c,g * f] and
A3: for a being LATTICE st a in F₁() holds
P₁[a,a, id a]