for Y being non empty set
for PA, PB being a_partition of Y
for p0, x, y being set
for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0