consider P being non empty ClosedSubset of L, o1, o2 being BinOp of P such that
A1: ( o1 = H₂(L) || P & o2 = H₃(L) || P & LattStr(# the carrier of l,the L_join of l,the L_meet of l #) = LattStr(# P,o1,o2 #) ) by Def15;
l .: is Sublattice of L .:

proof

take P .: ; :: according to FILTER_2:def 15 :: thesis: ex o1, o2 being BinOp of P .: st
( o1 = the L_join of (L .: ) || (P .: ) & o2 = the L_meet of (L .: ) || (P .: ) & LattStr(# the carrier of (l .: ),the L_join of (l .: ),the L_meet of (l .: ) #) = LattStr(# (P .: ),o1,o2 #) )
thus ex o1, o2 being BinOp of P .: st
( o1 = the L_join of (L .: ) || (P .: ) & o2 = the L_meet of (L .: ) || (P .: ) & LattStr(# the carrier of (l .: ),the L_join of (l .: ),the L_meet of (l .: ) #) = LattStr(# (P .: ),o1,o2 #) ) by A1; :: thesis: verum

end;

hence l .: is strict Sublattice of L .: ; :: thesis: verum