A7:
for a, b being Object of F1() st F3(a) = F3(b) holds
a = b
proof
let a,
b be
Object of
F1();
( F3(a) = F3(b) implies a = b )
(
a = latt a &
b = latt b )
;
hence
(
F3(
a)
= F3(
b) implies
a = b )
by A4;
verum
end;
A8:
now for a, b being Object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )let a,
b be
Object of
F2();
( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being Object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) ) )assume A9:
<^a,b^> <> {}
;
for f being Morphism of a,b ex c, d being Object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )let f be
Morphism of
a,
b;
ex c, d being Object of F1() ex g being Morphism of c,d st
( b = F3(c) & a = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )A10:
@ f = f
by A9, Def7;
then
P2[
latt a,
latt b,
@ f]
by A2, A9;
then consider c,
d being
LATTICE,
g being
Function of
c,
d such that A11:
(
c in the
carrier of
F1() &
d in the
carrier of
F1() )
and A12:
P1[
c,
d,
g]
and A13:
(
latt b = F3(
c) &
latt a = F3(
d) &
@ f = F4(
c,
d,
g) )
by A6;
reconsider c9 =
c,
d9 =
d as
Object of
F1()
by A11;
g in <^c9,d9^>
by A1, A12;
hence
ex
c,
d being
Object of
F1() ex
g being
Morphism of
c,
d st
(
b = F3(
c) &
a = F3(
d) &
<^c,d^> <> {} &
f = F4(
c,
d,
g) )
by A10, A13;
verum end;
A14:
for a, b being Object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g
proof
let a,
b be
Object of
F1();
( <^a,b^> <> {} implies for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g )
assume A15:
<^a,b^> <> {}
;
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g
let f,
g be
Morphism of
a,
b;
( F4(a,b,f) = F4(a,b,g) implies f = g )
(
@ f = f &
@ g = g )
by A15, Def7;
hence
(
F4(
a,
b,
f)
= F4(
a,
b,
g) implies
f = g )
by A5;
verum
end;
A16:
ex F being contravariant Functor of F1(),F2() st
( ( for a being Object of F1() holds F . a = F3(a) ) & ( for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4(a,b,f) ) )
by A3;
thus
F1(),F2() are_anti-isomorphic
from YELLOW18:sch 13(A16, A7, A14, A8); verum