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 S_{2}[a] holds

S_{1}[a,a, id a]
;

RelStr(# w, the well-ordering upper-bounded Order of w #) is complete ;

then A3: ex x being strict LATTICE st

( S_{2}[x] & the carrier of x in W )
;

A4: for a, b, c being LATTICE st S_{2}[a] & S_{2}[b] & S_{2}[c] holds

for f being Function of a,b

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

S_{1}[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 & S_{2}[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 S_{1}[ latt a, latt b,f] ) ) )
from YELLOW21:sch 3(A3, A4, A2); :: thesis: verum

set r = the well-ordering upper-bounded Order of w;

A2: for a being LATTICE st S

S

RelStr(# w, the well-ordering upper-bounded Order of w #) is complete ;

then A3: ex x being strict LATTICE st

( S

A4: for a, b, c being LATTICE st S

for f being Function of a,b

for g being Function of b,c st S

S

thus ex It being strict lattice-wise category st

( ( for x being LATTICE holds

( x is Object of It iff ( x is strict & S

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

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