:: deftheorem Def5 defines with_complete_lattices YELLOW21:def 5 :
for C being category holds
( C is with_complete_lattices iff ( C is lattice-wise & ( for a being Object of C holds a is complete LATTICE ) ) );