let L be antisymmetric with_infima lower-bounded RelStr ; :: thesis: for a being Element of L holds a "/\" (Bottom L) = Bottom L
let a be Element of L; :: thesis: a "/\" (Bottom L) = Bottom L
( Bottom L <= a "/\" (Bottom L) & a "/\" (Bottom L) <= Bottom L ) by YELLOW_0:23, YELLOW_0:44;
hence a "/\" (Bottom L) = Bottom L by YELLOW_0:def 3; :: thesis: verum