defpred S₁[ set , set , set ] means c₃ = c₃;
consider L being LATTICE;
A1: 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] ;
A2: for a being LATTICE st a in {L} holds
S₁[a,a, id a] ;
A3: for a being Element of {L} 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 = {L} & ( 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(A3, A1, A2);
reconsider C = C as strict lattice-wise category by A4;
take C ; :: thesis: C is with_all_isomorphisms
let a, b be object of C; :: according to YELLOW21:def 8 :: thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^>
let f be Function of (latt a),(latt b); :: thesis: ( f is isomorphic implies f in <^a,b^> )
thus ( f is isomorphic implies f in <^a,b^> ) by A5; :: thesis: verum