theorem Th4: :: WAYBEL_9:4

for L being reflexive antisymmetric with_suprema RelStr
for x being Element of L holds uparrow x = {x} "\/" ([#] L)