consider L being complete LATTICE;
defpred S₁[ set , set , set ] means c₃ = c₃;
A1: for a being Element of {L} holds a is LATTICE by TARSKI:def 1;
A2: for a, b, c being LATTICE st a in {L} & b in {L} & c in {L} holds
for f being Function of a,b
for g being Function of b,c st S₁[a,b,f] & S₁[b,c,g] holds
S₁[a,c,g * f] ;
A3: for a being LATTICE st a in {L} holds
S₁[a,a, id a] ;
consider C being strict category such that
A4: C is lattice-wise and
A5: the carrier of C = {L} 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 {L} & b in {L} & S₁[a,b,f] ) ) from YELLOW21:sch 1(A1, A2, A3);
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