let A be non empty Poset; :: thesis: for a being Element of
for S being Subset of holds not a in InitSegm S,a
let a be Element of ; :: thesis: for S being Subset of holds not a in InitSegm S,a
let S be Subset of ; :: 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 st
( a = a1 & ( for a2 being Element of st a2 in {a} holds
a1 < a2 ) ) ;
a in {a} by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum