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