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:12;
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 ) ;
then [s1,s3] in Path_Rel R by A1, RELAT_2:def 8;
hence s1 ~= s3 ; :: thesis: verum