theorem Th78: :: WAYBEL_1:78

for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c)