let A1, A2 be lattice-wise category; :: thesis: ( ( for x being LATTICE holds
( x is Object of A1 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being Object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[a,b,f] ) ) & ( for x being LATTICE holds
( x is Object of A2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being Object of A2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[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 & P1[x] & the carrier of x in F1() ) ) 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 P2[a,b,f] ) and
A3: for x being LATTICE holds
( x is Object of A2 iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ; :: thesis: ( ex a, b being Object of A2 ex f being monotone Function of (latt a),(latt b) st
( ( f in <^a,b^> implies P2[a,b,f] ) implies ( P2[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
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of A1 c= 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 & P1[x] ) by A3, A5;
A8: x as_1-sorted = x by A6, Def1;
then the carrier of (x as_1-sorted) in F1() by A3, A5, A6;
then x is Object of A1 by A1, A8, A7;
hence x in the carrier of A1 ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A1 or x in the carrier of A2 )
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 & P1[x] ) by A1, A9;
A12: x as_1-sorted = x by A10, Def1;
then the carrier of (x as_1-sorted) in F1() 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 C1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[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 P2[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 P2[a,b,f] ) implies ( P2[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