defpred S_{1}[ set , set , set ] means c_{3} = c_{3};

set L = the complete LATTICE;

A1: for a, b, c being LATTICE st a in { the complete LATTICE} & b in { the complete LATTICE} & c in { the complete LATTICE} holds

for f being Function of a,b

for g being Function of b,c st S_{1}[a,b,f] & S_{1}[b,c,g] holds

S_{1}[a,c,g * f]
;

A2: for a being LATTICE st a in { the complete LATTICE} holds

S_{1}[a,a, id a]
;

A3: for a being Element of { the complete LATTICE} holds a is LATTICE by TARSKI:def 1;

consider C being strict category such that

A4: C is lattice-wise and

A5: the carrier of C = { the complete LATTICE} and

for a, b being LATTICE

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in { the complete LATTICE} & b in { the complete LATTICE} & S_{1}[a,b,f] ) )
from YELLOW21:sch 1(A3, A1, A2);

take C ; :: thesis: ( C is strict & C is with_complete_lattices )

thus C is strict ; :: thesis: C is with_complete_lattices

thus C is lattice-wise by A4; :: according to YELLOW21:def 5 :: thesis: for a being Object of C holds a is complete LATTICE

let a be Object of C; :: thesis: a is complete LATTICE

thus a is complete LATTICE by A5, TARSKI:def 1; :: thesis: verum

set L = the complete LATTICE;

A1: for a, b, c being LATTICE st a in { the complete LATTICE} & b in { the complete LATTICE} & c in { the complete LATTICE} holds

for f being Function of a,b

for g being Function of b,c st S

S

A2: for a being LATTICE st a in { the complete LATTICE} holds

S

A3: for a being Element of { the complete LATTICE} holds a is LATTICE by TARSKI:def 1;

consider C being strict category such that

A4: C is lattice-wise and

A5: the carrier of C = { the complete LATTICE} and

for a, b being LATTICE

for f being monotone Function of a,b holds

( f in the Arrows of C . (a,b) iff ( a in { the complete LATTICE} & b in { the complete LATTICE} & S

take C ; :: thesis: ( C is strict & C is with_complete_lattices )

thus C is strict ; :: thesis: C is with_complete_lattices

thus C is lattice-wise by A4; :: according to YELLOW21:def 5 :: thesis: for a being Object of C holds a is complete LATTICE

let a be Object of C; :: thesis: a is complete LATTICE

thus a is complete LATTICE by A5, TARSKI:def 1; :: thesis: verum