theorem Th10: :: WAYBEL12:10

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