theorem :: YELLOW_5:21

for L being antisymmetric with_suprema lower-bounded RelStr
for a, b being Element of L st a "\/" b = Bottom L holds
( a = Bottom L & b = Bottom L )