theorem Th36: :: FLEXARY1:36
for D1, D2 being finite set st D1 misses D2 holds
for o1 being DoubleReorganization of D1
for o2 being DoubleReorganization of D2 holds o1 ^ o2 is DoubleReorganization of D1 \/ D2