let O be non empty connected Poset; :: thesis: for T being non empty array of O
for p, q, s being Element of dom T st p in s & s in q holds
( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )
let T be non empty array of O; :: thesis: for p, q, s being Element of dom T st p in s & s in q holds
( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )
let p, q, s be Element of dom T; :: thesis: ( p in s & s in q implies ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] ) )
assume ( p in s & s in q ) ; :: thesis: ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )
then ( p c= s & s c= q ) by ORDINAL1:def 2;
hence ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] ) by Th62; :: thesis: verum