:: deftheorem defines ~= OSALG_4:def 4 :
for R being non empty Poset
for s1, s2 being Element of R holds
( s1 ~= s2 iff [s1,s2] in Path_Rel R );