A7:
for a, b being Object of F_{1}() st F_{3}(a) = F_{3}(b) holds

a = b_{1}() st <^a,b^> <> {} holds

for f, g being Morphism of a,b st F_{4}(a,b,f) = F_{4}(a,b,g) holds

f = g_{1}(),F_{2}() st

( ( for a being Object of F_{1}() holds F . a = F_{3}(a) ) & ( for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}(a,b,f) ) )
by A3;

thus F_{1}(),F_{2}() are_anti-isomorphic
from YELLOW18:sch 13(A16, A7, A14, A8); :: thesis: verum

a = b

proof

let a, b be Object of F_{1}(); :: thesis: ( F_{3}(a) = F_{3}(b) implies a = b )

( a = latt a & b = latt b ) ;

hence ( F_{3}(a) = F_{3}(b) implies a = b )
by A4; :: thesis: verum

end;( a = latt a & b = latt b ) ;

hence ( F

A8: now :: thesis: for a, b being Object of F_{2}() st <^a,b^> <> {} holds

for f being Morphism of a,b ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( b = F_{3}(c) & a = F_{3}(d) & <^c,d^> <> {} & f = F_{4}(c,d,g) )

A14:
for a, b being Object of Ffor f being Morphism of a,b ex c, d being Object of F

( b = F

let a, b be Object of F_{2}(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( b = F_{3}(c) & a = F_{3}(d) & <^c,d^> <> {} & f = F_{4}(c,d,g) ) )

assume A9: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( b = F_{3}(c) & a = F_{3}(d) & <^c,d^> <> {} & f = F_{4}(c,d,g) )

let f be Morphism of a,b; :: thesis: ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( b = F_{3}(c) & a = F_{3}(d) & <^c,d^> <> {} & f = F_{4}(c,d,g) )

A10: @ f = f by A9, Def7;

then P_{2}[ 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 F_{1}() & d in the carrier of F_{1}() )
and

A12: P_{1}[c,d,g]
and

A13: ( latt b = F_{3}(c) & latt a = F_{3}(d) & @ f = F_{4}(c,d,g) )
by A6;

reconsider c9 = c, d9 = d as Object of F_{1}() by A11;

g in <^c9,d9^> by A1, A12;

hence ex c, d being Object of F_{1}() ex g being Morphism of c,d st

( b = F_{3}(c) & a = F_{3}(d) & <^c,d^> <> {} & f = F_{4}(c,d,g) )
by A10, A13; :: thesis: verum

end;( b = F

assume A9: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b ex c, d being Object of F

( b = F

let f be Morphism of a,b; :: thesis: ex c, d being Object of F

( b = F

A10: @ f = f by A9, Def7;

then P

then consider c, d being LATTICE, g being Function of c,d such that

A11: ( c in the carrier of F

A12: P

A13: ( latt b = F

reconsider c9 = c, d9 = d as Object of F

g in <^c9,d9^> by A1, A12;

hence ex c, d being Object of F

( b = F

for f, g being Morphism of a,b st F

f = g

proof

A16:
ex F being contravariant Functor of F
let a, b be Object of F_{1}(); :: thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F_{4}(a,b,f) = F_{4}(a,b,g) holds

f = g )

assume A15: <^a,b^> <> {} ; :: thesis: for f, g being Morphism of a,b st F_{4}(a,b,f) = F_{4}(a,b,g) holds

f = g

let f, g be Morphism of a,b; :: thesis: ( F_{4}(a,b,f) = F_{4}(a,b,g) implies f = g )

( @ f = f & @ g = g ) by A15, Def7;

hence ( F_{4}(a,b,f) = F_{4}(a,b,g) implies f = g )
by A5; :: thesis: verum

end;f = g )

assume A15: <^a,b^> <> {} ; :: thesis: for f, g being Morphism of a,b st F

f = g

let f, g be Morphism of a,b; :: thesis: ( F

( @ f = f & @ g = g ) by A15, Def7;

hence ( F

( ( for a being Object of F

for f being Morphism of a,b holds F . f = F

thus F