theorem Th1: :: GROUP_17:1

for A, B, A1, B1 being set st A misses B & A1 c= A & B1 c= B & A1 \/ B1 = A \/ B holds
( A1 = A & B1 = B )