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

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

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 X or q in {(Bottom L)} "\/" X )
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;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

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