let x, y, z be LD-EqClass; :: thesis: x 'or' (y '&' z) = (x 'or' y) '&' (x 'or' z)
thus x 'or' (y '&' z) = 'not' (('not' x) '&' (('not' y) 'or' ('not' z)))
.= 'not' ((('not' x) '&' ('not' y)) 'or' (('not' x) '&' ('not' z))) by Th104
.= (x 'or' y) '&' (x 'or' z) ; :: thesis: verum