theorem Th23: :: MEASUR10:1

for A, A1, A2, B, B1, B2 being non empty set holds
( ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] ) iff ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) )