let C1, C2 be strict lattice-wise category; ( ( 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 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 sups-preserving ) ) implies C1 = C2 )
assume that
A5:
for x being LATTICE holds
( x is Object of C1 iff ( x is strict & S1[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 sups-preserving )
and
A7:
for x being LATTICE holds
( x is Object of C2 iff ( x is strict & S1[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 sups-preserving )
; 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 sups-preserving );
A9:
now 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;
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);
( f in <^a,b^> iff S3[a,b,f] )
(
f in <^a,b^> iff
f is
sups-preserving )
by A6;
hence
(
f in <^a,b^> iff
S3[
a,
b,
f] )
;
verum end;
A10:
now 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;
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);
( f in <^a,b^> iff S3[a,b,f] )
(
f in <^a,b^> iff
f is
sups-preserving )
by A8;
hence
(
f in <^a,b^> iff
S3[
a,
b,
f] )
;
verum end;
for C1, C2 being lattice-wise category st ( for x being LATTICE holds
( x is Object of C1 iff ( x is strict & S1[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 & S1[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 YELLOW21:sch 5();
hence
C1 = C2
by A5, A7, A9, A10; verum