let R be non empty Poset; :: thesis: for s1, s2 being Element of R st s1 <= s2 holds
[s1,s2] in Path_Rel R
let s1, s2 be Element of R; :: thesis: ( s1 <= s2 implies [s1,s2] in Path_Rel R )
assume A1: s1 <= s2 ; :: thesis: [s1,s2] in Path_Rel R
set p = <*s1,s2*>;
A2: len <*s1,s2*> = 2 by FINSEQ_1:44;
A3: <*s1,s2*> . 1 = s1 ;
A4: for n being Nat st 2 <= n & n <= len <*s1,s2*> & not [(<*s1,s2*> . n),(<*s1,s2*> . (n - 1))] in the InternalRel of R holds
[(<*s1,s2*> . (n - 1)),(<*s1,s2*> . n)] in the InternalRel of R

proof

let n1 be Nat; :: thesis: ( 2 <= n1 & n1 <= len <*s1,s2*> & not [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R implies [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R )
assume ( 2 <= n1 & n1 <= len <*s1,s2*> ) ; :: thesis: ( [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R or [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R )
then A5: n1 = 2 by A2, XXREAL_0:1;
[s1,s2] in the InternalRel of R by A1, ORDERS_2:def 5;
hence ( [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R or [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R ) by A5; :: thesis: verum

end;

<*s1,s2*> . (len <*s1,s2*>) = s2 by A2;
hence [s1,s2] in Path_Rel R by A2, A3, A4, Def3; :: thesis: verum