theorem Th1: :: JORDAN1D:1

for A, B being set st ( for x being set st x in A holds
ex K being set st
( K c= B & x c= union K ) ) holds
union A c= union B