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 object ; :: 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 a9 being Element of L such that
A1: a9 = a and
A2: ex y being Element of L st
( a9 <= y & y in {(Bottom L)} ) ;
consider y being Element of L such that
A3: a9 <= y and
A4: y in {(Bottom L)} by A2;
A5: Bottom L <= a9 by YELLOW_0:44;
y = Bottom L by A4, TARSKI:def 1;
hence a in {(Bottom L)} by A1, A3, A4, A5, ORDERS_2:2; :: thesis: verum
end;
let a be object ; :: 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