let O be non empty connected Poset; :: thesis: 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]
let T be non empty array of O; :: thesis: 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]
let p, q, r, s be Element of dom T; :: thesis: ( p in q & r <> p & r <> q & s <> p & s <> q implies ((T,p,q) incl) . (r,s) = [r,s] )
assume A1: ( p in q & r <> p & r <> q & s <> p & s <> q ) ; :: thesis: ((T,p,q) incl) . (r,s) = [r,s]
set X = dom T;
set i = id (dom T);
set f = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
thus ((T,p,q) incl) . (r,s) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . s)] by A1, Th63
.= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . s)] by A1, Th33
.= [((id (dom T)) . r),((id (dom T)) . s)] by A1, Th33
.= [r,((id (dom T)) . s)]
.= [r,s] ; :: thesis: verum