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 : ex y being Element of st
( x <= y & y in {(Bottom L)} ) } by WAYBEL_0:14;
then consider a' being Element of such that
A1: a' = a and
A2: ex y being Element of st
( a' <= y & y in {(Bottom L)} ) ;
consider y being Element of such that
A3: a' <= y and
A4: y in {(Bottom L)} by A2;
A5: Bottom L <= a' by YELLOW_0:44;
y = Bottom L by A4, TARSKI:def 1;
hence a in {(Bottom L)} by A1, A3, A4, A5, 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 A6: a = Bottom L by TARSKI:def 1;
Bottom L <= Bottom L ;
hence a in downarrow (Bottom L) by A6, WAYBEL_0:17; :: thesis: verum