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

proof

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;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in X or q in {(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