let O be non empty connected Poset; :: thesis: for T being non empty array of O
for p, r, q being Element of dom T st p c= r & r c= q holds
( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )
let T be non empty array of O; :: thesis: for p, r, q being Element of dom T st p c= r & r c= q holds
( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )
let p, r, q be Element of dom T; :: thesis: ( p c= r & r c= q implies ( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] ) )
assume Z0: ( p c= r & r c= q ) ; :: thesis: ( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
( p in {p} & q in {q} & r in (succ q) \ p ) by Z0, TT, TARSKI:def 1;
then ( [p,r] in [:{p},((succ q) \ p):] & [r,q] in [:((succ q) \ p),{q}:] ) by ZFMISC_1:def 2;
then A1: ( [p,r] in [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] & [r,q] in [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] ) by XBOOLE_0:def 3;
A2: dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) = [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] by RELAT_1:45;
hence ((T,p,q) incl) . (p,r) = (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) . (p,r) by A1, FUNCT_4:13
.= [p,r] by A1, FUNCT_1:17 ;
:: thesis: ((T,p,q) incl) . (r,q) = [r,q]
thus ((T,p,q) incl) . (r,q) = (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) . (r,q) by A1, A2, FUNCT_4:13
.= [r,q] by A1, FUNCT_1:17 ; :: thesis: verum