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