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_isomorphic
from YELLOW18:sch 11(A19, 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

( a = F_{3}(c) & b = 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

( a = 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

( a = F_{3}(c) & b = 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

( a = F_{3}(c) & b = 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

( a = F_{3}(c) & b = 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 a = F_{3}(c) & latt b = 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

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

end;( a = F

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

( a = F

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

( a = 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 a = 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

( a = F

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

f = g

proof

A19:
ex F being covariant 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 )

A16: @ g = g by A15, Def7;

then A17: P_{1}[ latt a, latt b, @ g]
by A1, A15;

A18: @ f = f by A15, Def7;

then P_{1}[ latt a, latt b, @ f]
by A1, A15;

hence ( F_{4}(a,b,f) = F_{4}(a,b,g) implies f = g )
by A5, A18, A16, A17; :: 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

A16: @ g = g by A15, Def7;

then A17: P

A18: @ f = f by A15, Def7;

then P

hence ( F

( ( for a being Object of F

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

thus F