theorem Th10: :: WAYBEL14:10

for L being non empty antisymmetric lower-bounded RelStr holds uparrow (Bottom L) = the carrier of L