:: deftheorem defines .: FILTER_2:def 3 :
for L being Lattice
for p being Element of (L .:) holds .: p = p;