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