:: deftheorem defines ~ LATTICE3:def 7 :
for A being RelStr
for a being Element of (A ~) holds ~ a = a;