for Y being non empty set
for x, z0, t being set
for PA, PB being a_partition of Y st x in PA '\/' PB & z0 in PA & t in x & t in z0 holds
z0 c= x by Th16, Th18;