theorem Th2: :: OSALG_4:2

for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
[s1,s2] in Path_Rel R