theorem Th53: :: NORMFORM:53

for A being set
for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)