:: deftheorem defines InitSegm ORDERS_2:def 10 :
for A being non empty Poset
for S being Subset of A
for a being Element of A holds InitSegm (S,a) = (LowerCone {a}) /\ S;