:: deftheorem defines % LATTICE3:def 3 :
for L being Lattice
for p being Element of L holds p % = p;