let L be non empty lower-bounded Poset; :: thesis: downarrow (Bottom L) = {(Bottom L)}
thus downarrow (Bottom L) c= {(Bottom L)} :: according to XBOOLE_0:def 10 :: thesis: {(Bottom L)} c= downarrow (Bottom L)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in downarrow (Bottom L) or a in {(Bottom L)} )
assume a in downarrow (Bottom L) ; :: thesis: a in {(Bottom L)}
then a in { x where x is Element of L : ex y being Element of L st
( x <= y & y in {(Bottom L)} ) } by WAYBEL_0:14;
then consider a' being Element of L such that
A1: ( a' = a & ex y being Element of L st
( a' <= y & y in {(Bottom L)} ) ) ;
consider y being Element of L such that
A2: ( a' <= y & y in {(Bottom L)} ) by A1;
A3: Bottom L <= a' by YELLOW_0:44;
y = Bottom L by A2, TARSKI:def 1;
hence a in {(Bottom L)} by A1, A2, A3, ORDERS_2:25; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {(Bottom L)} or a in downarrow (Bottom L) )
assume a in {(Bottom L)} ; :: thesis: a in downarrow (Bottom L)
then A4: a = Bottom L by TARSKI:def 1;
Bottom L <= Bottom L ;
hence a in downarrow (Bottom L) by A4, WAYBEL_0:17; :: thesis: verum