theorem :: WAYBEL_1:85

for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b)