let A be non empty Poset; :: thesis: for a, b being Element of A
for S being Subset of A holds
( a in InitSegm (S,b) iff ( a < b & a in S ) )
let a, b be Element of A; :: thesis: for S being Subset of A holds
( a in InitSegm (S,b) iff ( a < b & a in S ) )
let S be Subset of A; :: thesis: ( a in InitSegm (S,b) iff ( a < b & a in S ) )
( a in InitSegm (S,b) iff ( a in LowerCone {b} & a in S ) ) by XBOOLE_0:def 4;
hence ( a in InitSegm (S,b) iff ( a < b & a in S ) ) by Th23; :: thesis: verum