theorem Th62: :: EXCHSORT:62

for O being non empty connected Poset
for T being non empty array of O
for p, q, r being Element of dom T st p c= r & r c= q holds
( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )