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