:: deftheorem defines (. FILTER_2:def 6 :
for L being Lattice holds (.L.> = the carrier of L;