theorem Th69: :: EXCHSORT:69

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