let O be non empty connected Poset; :: thesis: for T being non empty array of O
for r, p, q being Element of dom T st r in p & p in q holds
( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )
let T be non empty array of O; :: thesis: for r, p, q being Element of dom T st r in p & p in q holds
( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )
let r, p, q be Element of dom T; :: thesis: ( r in p & p in q implies ( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] ) )
assume Z0: ( r in p & p in q ) ; :: thesis: ( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )
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;
A0: dom (id (dom T)) = dom T by RELAT_1:45;
A2: ( r <> p & r <> q ) by Z0;
thus ((T,p,q) incl) . (r,p) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . p)] by Z0, FF6
.= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . p)] by A2, TSc
.= [r,((Swap ((id (dom T)),p,q)) . p)] by FUNCT_1:17
.= [r,((id (dom T)) . q)] by A0, TSa
.= [r,q] by FUNCT_1:17 ; :: thesis: ((T,p,q) incl) . (r,q) = [r,p]
thus ((T,p,q) incl) . (r,q) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . q)] by Z0, FF6
.= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . q)] by A2, TSc
.= [r,((Swap ((id (dom T)),p,q)) . q)] by FUNCT_1:17
.= [r,((id (dom T)) . p)] by A0, TSb
.= [r,p] by FUNCT_1:17 ; :: thesis: verum