reconsider w = w as non empty set by A1;
set r = the well-ordering upper-bounded Order of w;
A2:
for a being LATTICE st S2[a] holds
S1[a,a, id a]
;
RelStr(# w, the well-ordering upper-bounded Order of w #) is complete
;
then A3:
ex x being strict LATTICE st
( S2[x] & the carrier of x in W )
;
A4:
for a, b, c being LATTICE st S2[a] & S2[b] & S2[c] holds
for f being Function of a,b
for g being Function of b,c st S1[a,b,f] & S1[b,c,g] holds
S1[a,c,g * f]
by WAYBEL20:28;
thus
ex It being strict lattice-wise category st
( ( for x being LATTICE holds
( x is Object of It iff ( x is strict & S2[x] & the carrier of x in W ) ) ) & ( for a, b being Object of It
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S1[ latt a, latt b,f] ) ) )
from YELLOW21:sch 3(A3, A4, A2); verum