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

end;

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