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