A4:
for a being LATTICE st a in F_{1}() holds

P_{1}[a,a, id a]
by A3;

A5: for a, b, c being LATTICE st a in F_{1}() & b in F_{1}() & c in F_{1}() holds

for f being Function of a,b

for g being Function of b,c st P_{1}[a,b,f] & P_{1}[b,c,g] holds

P_{1}[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_{1}()
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_{1}() & b in F_{1}() & P_{1}[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_{1}() & ( for a, b being Object of C

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{1}[ latt a, latt b,f] ) ) )

thus the carrier of C = F_{1}()
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_{1}[ 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_{1}[ latt a, latt b,f] )

thus for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{1}[ latt a, latt b,f] )
by A7, A8; :: thesis: verum

P

A5: for a, b, c being LATTICE st a in F

for f being Function of a,b

for g being Function of b,c st P

P

consider C being strict category such that

A6: C is lattice-wise and

A7: the carrier of C = F

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

reconsider C = C as strict lattice-wise category by A6;

take C ; :: thesis: ( the carrier of C = F

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

thus the carrier of C = F

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

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

thus for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P