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