let B be non empty subcategory of A; :: thesis: B is with_complete_lattices
thus B is lattice-wise ; :: according to YELLOW21:def 5 :: thesis: for a being Object of B holds a is complete LATTICE
let b be Object of B; :: thesis: b is complete LATTICE
reconsider a = b as Object of A by ALTCAT_2:29;
a is complete LATTICE by Def5;
hence b is complete LATTICE ; :: thesis: verum