set C = W -UPS_category ;

thus W -UPS_category is lattice-wise ; :: according to YELLOW21:def 5 :: thesis: ( ( for a being Object of (W -UPS_category) holds a is complete LATTICE ) & W -UPS_category is with_all_isomorphisms )

A1: ex w being non empty set st w in W by SETFAM_1:def 10;

f in <^a,b^>

let f be Function of (latt a),(latt b); :: thesis: ( f is isomorphic implies f in <^a,b^> )

reconsider S = latt a, T = latt b as complete LATTICE by A1, Def10;

assume f is isomorphic ; :: thesis: f in <^a,b^>

then f is sups-preserving Function of S,T by WAYBEL13:20;

hence f in <^a,b^> by A1, Def10; :: thesis: verum

thus W -UPS_category is lattice-wise ; :: according to YELLOW21:def 5 :: thesis: ( ( for a being Object of (W -UPS_category) holds a is complete LATTICE ) & W -UPS_category is with_all_isomorphisms )

A1: ex w being non empty set st w in W by SETFAM_1:def 10;

hereby :: thesis: W -UPS_category is with_all_isomorphisms

let a, b be Object of (W -UPS_category); :: according to YELLOW21:def 8 :: thesis: for f being Function of (latt a),(latt b) st f is isomorphic holds let a be Object of (W -UPS_category); :: thesis: a is complete LATTICE

a = latt a ;

hence a is complete LATTICE by A1, Def10; :: thesis: verum

end;a = latt a ;

hence a is complete LATTICE by A1, Def10; :: thesis: verum

f in <^a,b^>

let f be Function of (latt a),(latt b); :: thesis: ( f is isomorphic implies f in <^a,b^> )

reconsider S = latt a, T = latt b as complete LATTICE by A1, Def10;

assume f is isomorphic ; :: thesis: f in <^a,b^>

then f is sups-preserving Function of S,T by WAYBEL13:20;

hence f in <^a,b^> by A1, Def10; :: thesis: verum