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

proof

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

end;

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