theorem :: WAYBEL12:15

for L being lower-bounded with_suprema Poset
for X being Subset of L holds {(Bottom L)} "\/" X = X