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 & S2[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 & S2[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 S3[ 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 );
A9: now :: thesis: for a, b being Object of C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )
let a, b be Object of C1; :: thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )

let f be monotone Function of (latt a),(latt b); :: thesis: ( f in <^a,b^> iff S3[a,b,f] )
( f in <^a,b^> iff f is directed-sups-preserving ) by A6;
hence ( f in <^a,b^> iff S3[a,b,f] ) ; :: thesis: verum
end;
A10: now :: thesis: for a, b being Object of C2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )
let a, b be Object of C2; :: thesis: for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff S3[a,b,f] )

let f be monotone Function of (latt a),(latt b); :: thesis: ( f in <^a,b^> iff S3[a,b,f] )
( f in <^a,b^> iff f is directed-sups-preserving ) by A8;
hence ( f in <^a,b^> iff S3[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 & S2[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 S3[a,b,f] ) ) & ( for x being LATTICE holds
( x is Object of C2 iff ( x is strict & S2[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 S3[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 hence C1 = C2 by A5, A7, A9, A10; :: thesis: verum