A7:
for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F_{4}(a,b,f) in the Arrows of F_{2}() . (F_{3}(b),F_{3}(a))
_{1}() holds F_{3}(a) is Object of F_{2}()
_{1}(),F_{2}() such that

A28: for a being Object of F_{1}() holds F . a = F_{3}(a)
and

A29: 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)
from YELLOW18:sch 9(A27, A7, A11, A25);

take F ; :: thesis: ( ( for a being Object of F_{1}() holds F . a = F_{3}((latt 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}((latt a),(latt b),(@ f)) ) )

thus for a being Object of F_{1}() holds F . a = F_{3}((latt a))
by A28; :: thesis: for a, b being Object of F_{1}() st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = F_{4}((latt a),(latt b),(@ f))

let a, b be Object of F_{1}(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = F_{4}((latt a),(latt b),(@ f)) )

assume A30: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F . f = F_{4}((latt a),(latt b),(@ f))

let f be Morphism of a,b; :: thesis: F . f = F_{4}((latt a),(latt b),(@ f))

f = @ f by A30, Def7;

hence F . f = F_{4}((latt a),(latt b),(@ f))
by A29, A30; :: thesis: verum

for f being Morphism of a,b holds F

proof

let a, b be Object of F_{1}(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F_{4}(a,b,f) in the Arrows of F_{2}() . (F_{3}(b),F_{3}(a)) )

assume A8: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F_{4}(a,b,f) in the Arrows of F_{2}() . (F_{3}(b),F_{3}(a))

let f be Morphism of a,b; :: thesis: F_{4}(a,b,f) in the Arrows of F_{2}() . (F_{3}(b),F_{3}(a))

A9: f = @ f by A8, Def7;

then P_{1}[a,b,f]
by A1, A8;

then A10: ( F_{4}(a,b,f) is Function of F_{3}(b),F_{3}(a) & P_{2}[F_{3}(b),F_{3}(a),F_{4}(a,b,f)] )
by A4, A9;

( F_{3}(a) in the carrier of F_{2}() & F_{3}(b) in the carrier of F_{2}() )
by A3, A9;

hence F_{4}(a,b,f) in the Arrows of F_{2}() . (F_{3}(b),F_{3}(a))
by A2, A10; :: thesis: verum

end;assume A8: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F

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

A9: f = @ f by A8, Def7;

then P

then A10: ( F

( F

hence F

A11: now :: thesis: for a, b, c being Object of F_{1}() st <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of F_{2}() st a9 = F_{3}(a) & b9 = F_{3}(b) & c9 = F_{3}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9

for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of F

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F

F

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

for g being Morphism of b,c

for a9, b9, c9 being Object of F_{2}() st a9 = F_{3}(a) & b9 = F_{3}(b) & c9 = F_{3}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9 )

assume that

A12: <^a,b^> <> {} and

A13: <^b,c^> <> {} ; :: thesis: for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of F_{2}() st a9 = F_{3}(a) & b9 = F_{3}(b) & c9 = F_{3}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c

for a9, b9, c9 being Object of F_{2}() st a9 = F_{3}(a) & b9 = F_{3}(b) & c9 = F_{3}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9

let g be Morphism of b,c; :: thesis: for a9, b9, c9 being Object of F_{2}() st a9 = F_{3}(a) & b9 = F_{3}(b) & c9 = F_{3}(c) holds

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9

let a9, b9, c9 be Object of F_{2}(); :: thesis: ( a9 = F_{3}(a) & b9 = F_{3}(b) & c9 = F_{3}(c) implies for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9 )

assume that

A14: a9 = F_{3}(a)
and

A15: b9 = F_{3}(b)
and

A16: c9 = F_{3}(c)
; :: thesis: for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9

let f9 be Morphism of b9,a9; :: thesis: for g9 being Morphism of c9,b9 st f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) holds

F_{4}(a,c,(g * f)) = f9 * g9

let g9 be Morphism of c9,b9; :: thesis: ( f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) implies F_{4}(a,c,(g * f)) = f9 * g9 )

assume A17: ( f9 = F_{4}(a,b,f) & g9 = F_{4}(b,c,g) )
; :: thesis: F_{4}(a,c,(g * f)) = f9 * g9

A18: F_{4}(a,b,f) in the Arrows of F_{2}() . (F_{3}(b),F_{3}(a))
by A7, A12;

then A19: @ f9 = f9 by A14, A15, Def7;

A20: @ g = g by A13, Def7;

then A21: P_{1}[b,c,g]
by A1, A13;

A22: F_{4}(b,c,g) in the Arrows of F_{2}() . (F_{3}(c),F_{3}(b))
by A7, A13;

then A23: @ g9 = g9 by A15, A16, Def7;

A24: @ f = f by A12, Def7;

then P_{1}[a,b,f]
by A1, A12;

then F_{4}(a,c,((@ g) * (@ f))) =
F_{4}(a,b,f) * F_{4}(b,c,g)
by A6, A24, A20, A21

.= f9 * g9 by A14, A15, A16, A17, A18, A22, A19, A23, Th3 ;

hence F_{4}(a,c,(g * f)) = f9 * g9
by A12, A13, Th3; :: thesis: verum

end;for g being Morphism of b,c

for a9, b9, c9 being Object of F

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F

F

assume that

A12: <^a,b^> <> {} and

A13: <^b,c^> <> {} ; :: thesis: for f being Morphism of a,b

for g being Morphism of b,c

for a9, b9, c9 being Object of F

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F

F

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c

for a9, b9, c9 being Object of F

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F

F

let g be Morphism of b,c; :: thesis: for a9, b9, c9 being Object of F

for f9 being Morphism of b9,a9

for g9 being Morphism of c9,b9 st f9 = F

F

let a9, b9, c9 be Object of F

for g9 being Morphism of c9,b9 st f9 = F

F

assume that

A14: a9 = F

A15: b9 = F

A16: c9 = F

for g9 being Morphism of c9,b9 st f9 = F

F

let f9 be Morphism of b9,a9; :: thesis: for g9 being Morphism of c9,b9 st f9 = F

F

let g9 be Morphism of c9,b9; :: thesis: ( f9 = F

assume A17: ( f9 = F

A18: F

then A19: @ f9 = f9 by A14, A15, Def7;

A20: @ g = g by A13, Def7;

then A21: P

A22: F

then A23: @ g9 = g9 by A15, A16, Def7;

A24: @ f = f by A12, Def7;

then P

then F

.= f9 * g9 by A14, A15, A16, A17, A18, A22, A19, A23, Th3 ;

hence F

A25: now :: thesis: for a being Object of F_{1}()

for a9 being Object of F_{2}() st a9 = F_{3}(a) holds

F_{4}(a,a,(idm a)) = idm a9

A27:
for a being Object of Ffor a9 being Object of F

F

let a be Object of F_{1}(); :: thesis: for a9 being Object of F_{2}() st a9 = F_{3}(a) holds

F_{4}(a,a,(idm a)) = idm a9

let a9 be Object of F_{2}(); :: thesis: ( a9 = F_{3}(a) implies F_{4}(a,a,(idm a)) = idm a9 )

assume A26: a9 = F_{3}(a)
; :: thesis: F_{4}(a,a,(idm a)) = idm a9

idm a = id (latt a) by Th2;

hence F_{4}(a,a,(idm a)) =
id (latt a9)
by A5, A26

.= idm a9 by Th2 ;

:: thesis: verum

end;F

let a9 be Object of F

assume A26: a9 = F

idm a = id (latt a) by Th2;

hence F

.= idm a9 by Th2 ;

:: thesis: verum

proof

consider F being strict contravariant Functor of F
let a be Object of F_{1}(); :: thesis: F_{3}(a) is Object of F_{2}()

a is LATTICE by Def4;

hence F_{3}(a) is Object of F_{2}()
by A3; :: thesis: verum

end;a is LATTICE by Def4;

hence F

A28: for a being Object of F

A29: for a, b being Object of F

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

take F ; :: thesis: ( ( for a being Object of F

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

thus for a being Object of F

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

let a, b be Object of F

assume A30: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F . f = F

let f be Morphism of a,b; :: thesis: F . f = F

f = @ f by A30, Def7;

hence F . f = F