A4: for a being LATTICE st a in F₁() holds
P₁[a,a, id a] by A3;
A5: 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] by A2;
consider C being strict category such that
A6: C is lattice-wise and
A7: the carrier of C = F₁() 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 F₁() & b in F₁() & P₁[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 = 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] ) ) )
thus the carrier of C = F₁() 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 P₁[ 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 P₁[ latt a, latt b,f] )
thus for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₁[ latt a, latt b,f] ) by A7, A8; :: thesis: verum