let R be non empty discrete Poset; :: thesis: for x, y being Element of R st [x,y] in Path_Rel R holds
x = y
let x, y be Element of R; :: thesis: ( [x,y] in Path_Rel R implies x = y )
assume [x,y] in Path_Rel R ; :: thesis: x = y
then consider p being FinSequence of the carrier of R such that
A1: 1 < len p and
A2: p . 1 = x and
A3: p . (len p) = y and
A4: for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R by Def3;
for n1 being Nat st 1 <= n1 & n1 <= len p holds
p . n1 = x

proof

defpred S₁[ Nat] means ( p . $1 <> x & 1 <= $1 );
let n1 be Nat; :: thesis: ( 1 <= n1 & n1 <= len p implies p . n1 = x )
assume that
A5: 1 <= n1 and
A6: n1 <= len p ; :: thesis: p . n1 = x
assume A7: p . n1 <> x ; :: thesis: contradiction
then A8: ex k being Nat st S₁[k] by A5;
consider k being Nat such that
A9: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A8);
1 < k by A2, A9, XXREAL_0:1;
then A10: 1 + 1 <= k by INT_1:7;
then A11: (1 + 1) - 1 <= k - 1 by XREAL_1:9;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3, XXREAL_0:2;
A12: p . k1 = x by A9, A11, XREAL_1:146;
k <= n1 by A5, A7, A9;
then A13: k <= len p by A6, XXREAL_0:2;
then k in dom p by A9, FINSEQ_3:25;
then reconsider pk = p . k as Element of R by PARTFUN1:4;

per cases ( [pk,x] in the InternalRel of R or [x,pk] in the InternalRel of R ) by A4, A10, A13, A12;

suppose [pk,x] in the InternalRel of R ; :: thesis: contradiction

then pk <= x by ORDERS_2:def 5;
hence contradiction by A9, ORDERS_3:1; :: thesis: verum

end;

suppose [x,pk] in the InternalRel of R ; :: thesis: contradiction

then x <= pk by ORDERS_2:def 5;
hence contradiction by A9, ORDERS_3:1; :: thesis: verum

end;

end;

end;

hence x = y by A1, A3; :: thesis: verum