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