A4:
for a being LATTICE st a in F1() holds
P1[a,a, id a]
by A3;
A5:
for a, b, c being LATTICE st a in F1() & b in F1() & c in F1() holds
for f being Function of a,b
for g being Function of b,c st P1[a,b,f] & P1[b,c,g] holds
P1[a,c,g * f]
by A2;
consider C being strict category such that
A6:
C is lattice-wise
and
A7:
the carrier of C = F1()
and
A8:
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 F1() & b in F1() & P1[a,b,f] ) )
from YELLOW21:sch 1(A1, A5, A4);
reconsider C = C as strict lattice-wise category by A6;
take
C
; ( the carrier of C = F1() & ( for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] ) ) )
thus
the carrier of C = F1()
by A7; for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] )
let a, b be Object of C; for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] )
thus
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] )
by A7, A8; verum