theorem :: FILTER_2:7

for L being Lattice holds (L .:) .: = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ;