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) by Th78;