theorem Th5: :: NORMFORM:5
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds a /\ (b \/ c) = (a /\ b) \/ (a /\ c)