theorem Th18: :: PARTIT1:18

for Y being non empty set
for x, z0, t being set
for PA, PC being a_partition of Y st PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds
z0 c= x