let L be upper-bounded Semilattice; :: thesis: for X being Subset of L holds {(Top L)} "/\" X = X

let X be Subset of L; :: thesis: {(Top L)} "/\" X = X

A1: {(Top L)} "/\" X = { ((Top L) "/\" y) where y is Element of L : y in X } by YELLOW_4:42;

thus {(Top L)} "/\" X c= X :: according to XBOOLE_0:def 10 :: thesis: X c= {(Top L)} "/\" X

assume A2: q in X ; :: thesis: q in {(Top L)} "/\" X

then reconsider X1 = X as non empty Subset of L ;

reconsider y = q as Element of X1 by A2;

q = (Top L) "/\" y by WAYBEL_1:4;

hence q in {(Top L)} "/\" X by A1; :: thesis: verum

let X be Subset of L; :: thesis: {(Top L)} "/\" X = X

A1: {(Top L)} "/\" X = { ((Top L) "/\" y) where y is Element of L : y in X } by YELLOW_4:42;

thus {(Top L)} "/\" X c= X :: according to XBOOLE_0:def 10 :: thesis: X c= {(Top L)} "/\" X

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in X or q in {(Top L)} "/\" X )
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {(Top L)} "/\" X or q in X )

assume q in {(Top L)} "/\" X ; :: thesis: q in X

then ex y being Element of L st

( q = (Top L) "/\" y & y in X ) by A1;

hence q in X by WAYBEL_1:4; :: thesis: verum

end;assume q in {(Top L)} "/\" X ; :: thesis: q in X

then ex y being Element of L st

( q = (Top L) "/\" y & y in X ) by A1;

hence q in X by WAYBEL_1:4; :: thesis: verum

assume A2: q in X ; :: thesis: q in {(Top L)} "/\" X

then reconsider X1 = X as non empty Subset of L ;

reconsider y = q as Element of X1 by A2;

q = (Top L) "/\" y by WAYBEL_1:4;

hence q in {(Top L)} "/\" X by A1; :: thesis: verum