:: deftheorem defines <. FILTER_0:def 1 :
for L being Lattice holds <.L.) = the carrier of L;