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

set L = the LATTICE;

A1: for a, b, c being LATTICE st a in { the LATTICE} & b in { the LATTICE} & c in { the 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 LATTICE} holds

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

A3: for a being Element of { the 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 LATTICE} & ( 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 LATTICE} & b in { the LATTICE} & S_{1}[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

set L = the LATTICE;

A1: for a, b, c being LATTICE st a in { the LATTICE} & b in { the LATTICE} & c in { the 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 LATTICE} holds

S

A3: for a being Element of { the 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 LATTICE} & ( 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 LATTICE} & b in { the LATTICE} & S

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