theorem Th65: :: EXCHSORT:65

for f being Function
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 q in r & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )