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