let B be non empty subcategory of non empty semi-functional para-functional set-id-inheriting concrete carrier-underlaid lattice-wise ; :: thesis: B is with_complete_lattices
thus B is lattice-wise ; :: according to YELLOW21:def 5 :: thesis: for a being object of holds a is complete LATTICE
let b be object of ; :: thesis: b is complete LATTICE
reconsider a = b as object of by ALTCAT_2:30;
a is complete LATTICE by Def5;
hence b is complete LATTICE ; :: thesis: verum