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 )
assume A1: ( s1 ~= s2 & s2 ~= s3 ) ; :: thesis: s1 ~= s3
set PR = Path_Rel R;
A2: ( [s1,s2] in Path_Rel R & [s2,s3] in Path_Rel R ) by A1, Def5;
field (Path_Rel R) = the carrier of R by ORDERS_1:97;
then Path_Rel R is_transitive_in the carrier of R by RELAT_2:def 16;
then [s1,s3] in Path_Rel R by A2, RELAT_2:def 8;
hence s1 ~= s3 by Def5; :: thesis: verum