ex C being strict lattice-wise category st
( ( for x being LATTICE holds
( x is Object of C iff ( x is strict & P₁[x] & the carrier of x in F₁() ) ) ) & ( for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₂[ latt a, latt b,f] ) ) )

A1: ex x being strict LATTICE st
( P₁[x] & the carrier of x in F₁() ) and
A2: for a, b, c being LATTICE st P₁[a] & P₁[b] & P₁[c] 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 P₁[a] holds
P₂[a,a, id a]