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

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