:: deftheorem defines \/ NORMFORM:def 2 :
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x \/ y = [((x `1) \/ (y `1)),((x `2) \/ (y `2))];