let A be non empty Poset; :: thesis: for a being Element of A
for S being Subset of A holds not a in InitSegm (S,a)
let a be Element of A; :: thesis: for S being Subset of A holds not a in InitSegm (S,a)
let S be Subset of A; :: thesis: not a in InitSegm (S,a)
assume a in InitSegm (S,a) ; :: thesis: contradiction
then a in LowerCone {a} by XBOOLE_0:def 4;
then A1: ex a1 being Element of A st
( a = a1 & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
a in {a} by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum