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