let O be non empty connected Poset; :: thesis: for T being non empty array of O
for p, q being Element of dom T holds (succ q) \ p c= dom T
let T be non empty array of O; :: thesis: for p, q being Element of dom T holds (succ q) \ p c= dom T
let p, q be Element of dom T; :: thesis: (succ q) \ p c= dom T
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (succ q) \ p or x in dom T )
reconsider xx = x as set by TARSKI:1;
assume A1: x in (succ q) \ p ; :: thesis: x in dom T
A2: ( p c= xx & xx c= q ) by A1, Th59;
consider a, b being Ordinal such that
A3: dom T = a \ b by Def1;
( q in a & p nin b ) by A3, XBOOLE_0:def 5;
then ( x in a & x nin b ) by A1, A2, ORDINAL1:12;
hence x in dom T by A3, XBOOLE_0:def 5; :: thesis: verum