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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in UpperCone ([#] A) or x in {} )
assume x in UpperCone ([#] A) ; :: thesis: x in {}
then consider a being Element of A such that
x = a and
A1: for a2 being Element of A st a2 in [#] A holds
a2 < a ;
thus x in {} by A1; :: thesis: verum
end;
thus {} c= UpperCone ([#] A) by XBOOLE_1:2; :: thesis: verum