theorem Th6: :: OSALG_4:6

for R being non empty discrete Poset
for x, y being Element of R st [x,y] in Path_Rel R holds
x = y