let L be antisymmetric lower-bounded with_infima RelStr ; :: thesis: for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)}
let X be non empty Subset of L; :: thesis: X "/\" {(Bottom L)} = {(Bottom L)}
A1: X "/\" {(Bottom L)} = { ((Bottom L) "/\" y) where y is Element of L : y in X } by YELLOW_4:42;
thus X "/\" {(Bottom L)} c= {(Bottom L)} by Th14; :: according to XBOOLE_0:def 10 :: thesis: {(Bottom L)} c= X "/\" {(Bottom L)}
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in {(Bottom L)} or q in X "/\" {(Bottom L)} )
assume q in {(Bottom L)} ; :: thesis: q in X "/\" {(Bottom L)}
then A2: q = Bottom L by TARSKI:def 1;
consider y being set such that
A3: y in X by XBOOLE_0:def 1;
reconsider y = y as Element of X by A3;
(Bottom L) "/\" y = Bottom L by WAYBEL_1:4;
hence q in X "/\" {(Bottom L)} by A1, A2; :: thesis: verum