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_{2}[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_{2}[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_{3}[ 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 );

( x is Object of C1 iff ( x is strict & S_{2}[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_{3}[a,b,f] ) ) & ( for x being LATTICE holds

( x is Object of C2 iff ( x is strict & S_{2}[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_{3}[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

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

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

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

( $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 S_{3}[a,b,f] )

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

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

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_{3}[a,b,f] )

let f be monotone Function of (latt a),(latt b); :: thesis: ( f in <^a,b^> iff S_{3}[a,b,f] )

( f in <^a,b^> iff f is directed-sups-preserving ) by A6;

hence ( f in <^a,b^> iff S_{3}[a,b,f] )
; :: thesis: verum

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

let f be monotone Function of (latt a),(latt b); :: thesis: ( f in <^a,b^> iff S

( f in <^a,b^> iff f is directed-sups-preserving ) by A6;

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

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 S_{3}[a,b,f] )

for C1, C2 being lattice-wise category st ( for x being LATTICE holds for f being monotone Function of (latt a),(latt b) holds

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

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_{3}[a,b,f] )

let f be monotone Function of (latt a),(latt b); :: thesis: ( f in <^a,b^> iff S_{3}[a,b,f] )

( f in <^a,b^> iff f is directed-sups-preserving ) by A8;

hence ( f in <^a,b^> iff S_{3}[a,b,f] )
; :: thesis: verum

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

let f be monotone Function of (latt a),(latt b); :: thesis: ( f in <^a,b^> iff S

( f in <^a,b^> iff f is directed-sups-preserving ) by A8;

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

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

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

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

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

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

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

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