theorem :: WAYBEL12:11

for L being antisymmetric lower-bounded with_infima RelStr
for X being non empty Subset of L holds X "/\" {(Bottom L)} = {(Bottom L)}