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