reconsider w = w as non empty set by A1;
let C1, C2 be strict lattice-wise category; :: thesis: ( ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) implies C1 = C2 )
assume that
A5: for x being LATTICE holds
( x is object of C1 iff ( x is strict & S₂[x] & the carrier of x in W ) ) and
A6: for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) and
A7: for x being LATTICE holds
( x is object of C2 iff ( x is strict & S₂[x] & the carrier of x in W ) ) and
A8: for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ; :: thesis: C1 = C2
defpred S₃[ set , set , set ] means ex L1, L2 being LATTICE ex f being Function of L1,L2 st
( $1 = L1 & $2 = L2 & $3 = f & f is directed-sups-preserving );
consider r being well-ordering upper-bounded Order of w;

A9: now

let a, b be object of C1; :: thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S₃[a,b,f] )
let f be monotone Function of (latt a),(latt b); :: thesis: ( f in <^a,b^> iff S₃[a,b,f] )
( f in <^a,b^> iff f is directed-sups-preserving ) by A6;
hence ( f in <^a,b^> iff S₃[a,b,f] ) ; :: thesis: verum

end;

A10: now

let a, b be object of C2; :: thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S₃[a,b,f] )
let f be monotone Function of (latt a),(latt b); :: thesis: ( f in <^a,b^> iff S₃[a,b,f] )
( f in <^a,b^> iff f is directed-sups-preserving ) by A8;
hence ( f in <^a,b^> iff S₃[a,b,f] ) ; :: thesis: verum

end;

for C1, C2 being lattice-wise category st ( for x being LATTICE holds
( x is object of C1 iff ( x is strict & S₂[x] & the carrier of x in W ) ) ) & ( for a, b being object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S₃[a,b,f] ) ) & ( for x being LATTICE holds
( x is object of C2 iff ( x is strict & S₂[x] & the carrier of x in W ) ) ) & ( for a, b being object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S₃[a,b,f] ) ) holds
AltCatStr(# the carrier of C1,the Arrows of C1,the Comp of C1 #) = AltCatStr(# the carrier of C2,the Arrows of C2,the Comp of C2 #) from YELLOW21:sch 5();
hence C1 = C2 by A5, A7, A9, A10; :: thesis: verum