let O be non empty connected Poset; :: thesis: for T being non empty array of O
for q, p being Element of dom T holds (succ q) \ p c= dom T
let T be non empty array of O; :: thesis: for q, p being Element of dom T holds (succ q) \ p c= dom T
let q, p be Element of dom T; :: thesis: (succ q) \ p c= dom T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (succ q) \ p or x in dom T )
assume Z0: x in (succ q) \ p ; :: thesis: x in dom T
A1: ( p c= x & x c= q ) by Z0, TT;
consider a, b being ordinal number such that
A2: dom T = a \ b by SEG;
( q in a & p nin b ) by A2, XBOOLE_0:def 5;
then ( x in a & x nin b ) by Z0, A1, ORDINAL1:12;
hence x in dom T by A2, XBOOLE_0:def 5; :: thesis: verum