set PR = Path_Rel R;
field (Path_Rel R) = the carrier of R by ORDERS_1:12;
then Path_Rel R is_reflexive_in the carrier of R by RELAT_2:def 9;
hence for s1 being Element of R holds [s1,s1] in Path_Rel R by RELAT_2:def 1; :: thesis: verum