theorem Th5: :: WAYBEL_9:5

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