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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: 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; :: thesis: verum