let L be non empty lower-bounded Poset; :: thesis: for I being Ideal of L holds Bottom L in I
let I be Ideal of L; :: thesis: Bottom L in I
set x = the Element of I;
Bottom L <= the Element of I by YELLOW_0:44;
hence Bottom L in I by WAYBEL_0:def 19; :: thesis: verum