theorem Th1: :: YELLOW_4:1

for L being RelStr
for X being set
for a being Element of L st a in X & ex_sup_of X,L holds
a <= "\/" (X,L)