theorem Th1: :: TEX_3:1

for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( not A is empty iff B is proper )