:: deftheorem Def8 defines with_all_isomorphisms YELLOW21:def 8 :
for C being lattice-wise category holds
( C is with_all_isomorphisms iff for a, b being Object of C
for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^> );