theorem Th67: :: EXCHSORT:67

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