defpred S₁[ set , set , set ] means c₃ = c₃;
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₁[a,b,f] & S₁[b,c,g] holds
S₁[a,c,g * f] ;
A2: for a being LATTICE st a in { the complete LATTICE} holds
S₁[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₁[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