A7:
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;
A8:
for a, b being object of F1() st F3(a) = F3(b) holds
a = b
A9:
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();
:: thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g )
assume A10:
<^a,b^> <> {}
;
:: thesis: 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;
:: thesis: ( F4(a,b,f) = F4(a,b,g) implies f = g )
(
latt a = a &
latt b = b &
@ f = f &
@ g = g )
by A10, Def7;
hence
(
F4(
a,
b,
f)
= F4(
a,
b,
g) implies
f = g )
by A5;
:: thesis: verum
end;
A11:
now let a,
b be
object of
F2();
:: thesis: ( <^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 A12:
<^a,b^> <> {}
;
:: thesis: 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;
:: thesis: 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) )A13:
(
latt a = a &
latt b = b &
@ f = f )
by A12, Def7;
then
P2[
latt a,
latt b,
@ f]
by A2, A12;
then consider c,
d being
LATTICE,
g being
Function of
c,
d such that A14:
(
c in the
carrier of
F1() &
d in the
carrier of
F1() &
P1[
c,
d,
g] &
latt b = F3(
c) &
latt a = F3(
d) &
@ f = F4(
c,
d,
g) )
by A6;
reconsider c' =
c,
d' =
d as
object of
F1()
by A14;
g in <^c',d'^>
by A1, A14;
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 A13, A14;
:: thesis: verum end;
thus
F1(),F2() are_anti-isomorphic
from YELLOW18:sch 13(A7, A8, A9, A11); :: thesis: verum