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

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