theorem Th24: :: YELLOW_2:24

for L being non empty RelStr st ( for X being set holds ex_sup_of X,L ) holds
L is complete