theorem :: YELLOW_0:45

for L being non empty antisymmetric upper-bounded RelStr
for x being Element of L holds x <= Top L