set PR = Path_Rel R;
field (Path_Rel R) = the carrier of R by ORDERS_1:12;
then Path_Rel R is_symmetric_in the carrier of R by RELAT_2:def 11;
hence for s1, s2 being Element of R st [s1,s2] in Path_Rel R holds
[s2,s1] in Path_Rel R by RELAT_2:def 3; :: thesis: verum