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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LowerCone ([#] A) or x in {} )
assume x in LowerCone ([#] 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
a < a2 ;
thus x in {} by A1; :: thesis: verum

end;

thus {} c= LowerCone ([#] A) by XBOOLE_1:2; :: thesis: verum