let A be non empty Poset; :: thesis: UpperCone ([#] A) = {}
thus UpperCone ([#] A) c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= UpperCone ([#] A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UpperCone ([#] A) or x in {} )
assume x in UpperCone ([#] A) ; :: thesis: x in {}
then ex a being Element of A st
( x = a & ( for a2 being Element of A st a2 in [#] A holds
a2 < a ) ) ;
hence x in {} ; :: thesis: verum

end;

thus {} c= UpperCone ([#] A) ; :: thesis: verum