let A be non empty Poset; :: thesis: for a, c being Element of A holds
( a < c iff a in LowerCone {c} )
let a, c be Element of A; :: thesis: ( a < c iff a in LowerCone {c} )
thus ( a < c implies a in LowerCone {c} ) :: thesis: ( a in LowerCone {c} implies a < c )

proof

assume a < c ; :: thesis: a in LowerCone {c}
then for b being Element of A st b in {c} holds
a < b by TARSKI:def 1;
hence a in LowerCone {c} ; :: thesis: verum

end;

assume a in LowerCone {c} ; :: thesis: a < c
then A1: ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in {c} holds
a1 < a2 ) ) ;
c in {c} by TARSKI:def 1;
hence a < c by A1; :: thesis: verum