A7: for a, b being Object of F1() st F3(a) = F3(b) holds
a = b
proof
let a, b be Object of F1(); :: thesis: ( F3(a) = F3(b) implies a = b )
( a = latt a & b = latt b ) ;
hence ( F3(a) = F3(b) implies a = b ) by A4; :: thesis: verum
end;
A8: now :: thesis: 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(); :: 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 A9: <^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) )

A10: @ f = f by ;
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 ;
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 ; :: thesis: 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(); :: 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 A15: <^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 )
( @ f = f & @ g = g ) by ;
hence ( F4(a,b,f) = F4(a,b,g) implies f = g ) by A5; :: thesis: 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 :: thesis: verum