let A1, A2 be lattice-wise category; :: thesis: ( ( for x being LATTICE holds

( x is Object of A1 iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) ) ) & ( for a, b being Object of A1

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

( f in <^a,b^> iff P_{2}[a,b,f] ) ) & ( for x being LATTICE holds

( x is Object of A2 iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) ) ) & ( for a, b being Object of A2

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

( f in <^a,b^> iff P_{2}[a,b,f] ) ) implies AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) )

assume that

A1: for x being LATTICE holds

( x is Object of A1 iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) )
and

A2: for a, b being Object of A1

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

( f in <^a,b^> iff P_{2}[a,b,f] )
and

A3: for x being LATTICE holds

( x is Object of A2 iff ( x is strict & P_{1}[x] & the carrier of x in F_{1}() ) )
; :: thesis: ( ex a, b being Object of A2 ex f being monotone Function of (latt a),(latt b) st

( ( f in <^a,b^> implies P_{2}[a,b,f] ) implies ( P_{2}[a,b,f] & not f in <^a,b^> ) ) or AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) )

A4: the carrier of A2 = the carrier of A1

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

( f in <^a,b^> iff P_{2}[a,b,f] ) ) & the carrier of C2 = the carrier of A1 & ( for a, b being Object of C2

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

( f in <^a,b^> iff P_{2}[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 4();

hence ( ex a, b being Object of A2 ex f being monotone Function of (latt a),(latt b) st

( ( f in <^a,b^> implies P_{2}[a,b,f] ) implies ( P_{2}[a,b,f] & not f in <^a,b^> ) ) or AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) )
by A2, A4; :: thesis: verum

( x is Object of A1 iff ( x is strict & P

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

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

( x is Object of A2 iff ( x is strict & P

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

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

assume that

A1: for x being LATTICE holds

( x is Object of A1 iff ( x is strict & P

A2: for a, b being Object of A1

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

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

A3: for x being LATTICE holds

( x is Object of A2 iff ( x is strict & P

( ( f in <^a,b^> implies P

A4: the carrier of A2 = the carrier of A1

proof

assume A9: x in the carrier of A1 ; :: thesis: x in the carrier of A2

then A10: x is LATTICE by Def4;

then A11: ( x is strict LATTICE & P_{1}[x] )
by A1, A9;

A12: x as_1-sorted = x by A10, Def1;

then the carrier of (x as_1-sorted) in F_{1}()
by A1, A9, A10;

then x is Object of A2 by A3, A12, A11;

hence x in the carrier of A2 ; :: thesis: verum

end;

for C1, C2 being lattice-wise category st the carrier of C1 = the carrier of A1 & ( for a, b being Object of C1hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of A1 c= the carrier of A2

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A1 or x in the carrier of A2 )let x be object ; :: thesis: ( x in the carrier of A2 implies x in the carrier of A1 )

assume A5: x in the carrier of A2 ; :: thesis: x in the carrier of A1

then A6: x is LATTICE by Def4;

then A7: ( x is strict LATTICE & P_{1}[x] )
by A3, A5;

A8: x as_1-sorted = x by A6, Def1;

then the carrier of (x as_1-sorted) in F_{1}()
by A3, A5, A6;

then x is Object of A1 by A1, A8, A7;

hence x in the carrier of A1 ; :: thesis: verum

end;assume A5: x in the carrier of A2 ; :: thesis: x in the carrier of A1

then A6: x is LATTICE by Def4;

then A7: ( x is strict LATTICE & P

A8: x as_1-sorted = x by A6, Def1;

then the carrier of (x as_1-sorted) in F

then x is Object of A1 by A1, A8, A7;

hence x in the carrier of A1 ; :: thesis: verum

assume A9: x in the carrier of A1 ; :: thesis: x in the carrier of A2

then A10: x is LATTICE by Def4;

then A11: ( x is strict LATTICE & P

A12: x as_1-sorted = x by A10, Def1;

then the carrier of (x as_1-sorted) in F

then x is Object of A2 by A3, A12, A11;

hence x in the carrier of A2 ; :: thesis: verum

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

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

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

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

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 4();

hence ( ex a, b being Object of A2 ex f being monotone Function of (latt a),(latt b) st

( ( f in <^a,b^> implies P