theorem Th1: :: PARTIT1:1

for Y being non empty set
for PA being a_partition of Y
for X, V being set st X in PA & V in PA & X c= V holds
X = V