let R be non empty Poset; :: thesis: for s1, s2, s3 being Element of R st s1 ~= s2 & s2 ~= s3 holds
s1 ~= s3
let s1, s2, s3 be Element of R; :: thesis: ( s1 ~= s2 & s2 ~= s3 implies s1 ~= s3 )
set PR = Path_Rel R;
field (Path_Rel R) = the carrier of R by ORDERS_1:97;
then A1: Path_Rel R is_transitive_in the carrier of R by RELAT_2:def 16;
assume ( s1 ~= s2 & s2 ~= s3 ) ; :: thesis: s1 ~= s3
then ( [s1,s2] in Path_Rel R & [s2,s3] in Path_Rel R ) by Def5;
then [s1,s3] in Path_Rel R by A1, RELAT_2:def 8;
hence s1 ~= s3 by Def5; :: thesis: verum