for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T holds (succ q) \ p c= dom T