let L be lower-bounded algebraic LATTICE; :: thesis: for S being CLSubFrame of L holds S is algebraic
let S be CLSubFrame of L; :: thesis: S is algebraic
RelStr(# the carrier of S, the InternalRel of S #) = Image (closure_op S) by WAYBEL10:18;
then RelStr(# the carrier of S, the InternalRel of S #) is algebraic by WAYBEL_8:24;
hence S is algebraic by WAYBEL_8:17; :: thesis: verum