theorem Th105: :: GRZLOG_1:48

for x, y, z being LD-EqClass holds x 'or' (y '&' z) = (x 'or' y) '&' (x 'or' z)