let L be lower-bounded with_suprema Poset; :: thesis: for X being Subset of L holds {(Bottom L)} "\/" X = X
let X be Subset of L; :: thesis: {(Bottom L)} "\/" X = X
A1: {(Bottom L)} "\/" X = { ((Bottom L) "\/" y) where y is Element of L : y in X } by YELLOW_4:15;
thus {(Bottom L)} "\/" X c= X :: according to XBOOLE_0:def 10 :: thesis: X c= {(Bottom L)} "\/" X

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {(Bottom L)} "\/" X or q in X )
assume q in {(Bottom L)} "\/" X ; :: thesis: q in X
then ex y being Element of L st
( q = (Bottom L) "\/" y & y in X ) by A1;
hence q in X by WAYBEL_1:3; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in X or q in {(Bottom L)} "\/" X )
assume A2: q in X ; :: thesis: q in {(Bottom L)} "\/" X
then reconsider X1 = X as non empty Subset of L ;
reconsider y = q as Element of X1 by A2;
q = (Bottom L) "\/" y by WAYBEL_1:3;
hence q in {(Bottom L)} "\/" X by A1; :: thesis: verum