let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: for X being non empty Subset of L holds Bottom L in downarrow X
let X be non empty Subset of L; :: thesis: Bottom L in downarrow X
A1: downarrow X = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } by WAYBEL_0:14;
consider y being set such that
A2: y in X by XBOOLE_0:def 1;
reconsider y = y as Element of X by A2;
Bottom L <= y by YELLOW_0:44;
hence Bottom L in downarrow X by A1; :: thesis: verum