theorem Th104: :: GRZLOG_1:47
for x, y, z being LD-EqClass holds x '&' (y 'or' z) = (x '&' y) 'or' (x '&' z)