let O be non empty connected Poset; for T being non empty array of O
for p, q, r 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; for p, q, r 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 p, q, r be Element of dom T; ( r in p & p in q implies ( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] ) )
assume A1:
( r in p & p in q )
; ( ((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;
A2:
dom (id (dom T)) = dom T
;
A3:
( r <> p & r <> q )
by A1;
thus ((T,p,q) incl) . (r,p) =
[((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . p)]
by A1, Th64
.=
[((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . p)]
by A3, Th33
.=
[r,((Swap ((id (dom T)),p,q)) . p)]
.=
[r,((id (dom T)) . q)]
by A2, Th29
.=
[r,q]
; ((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 A1, Th64
.=
[((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . q)]
by A3, Th33
.=
[r,((Swap ((id (dom T)),p,q)) . q)]
.=
[r,((id (dom T)) . p)]
by A2, Th31
.=
[r,p]
; verum