:: deftheorem defines .: FILTER_2:def 4 :
for L being Lattice
for X being Subset of L holds X .: = X;