:: deftheorem defines 'not' WAYBEL_1:def 22 :
for H being non empty RelStr
for a being Element of H holds 'not' a = a => (Bottom H);