:: deftheorem defines ^ NORMFORM:def 11 :
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;