let A be non empty Poset; :: thesis: UpperCone ({} A) = the carrier of A
thus UpperCone ({} A) c= the carrier of A ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of A c= UpperCone ({} A)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A or x in UpperCone ({} A) )
assume x in the carrier of A ; :: thesis: x in UpperCone ({} A)
then reconsider a = x as Element of A ;
for a2 being Element of A st a2 in {} A holds
a2 < a ;
hence x in UpperCone ({} A) ; :: thesis: verum