let A be non empty Poset; :: thesis: for a being Element of A holds not a in UpperCone {a}
let a be Element of A; :: thesis: not a in UpperCone {a}
a in {a} by TARSKI:def 1;
hence not a in UpperCone {a} by Th18; :: thesis: verum