let R be non empty Poset; for s1, s2 being Element of R st s1 <= s2 holds
[s1,s2] in Path_Rel R
let s1, s2 be Element of R; ( s1 <= s2 implies [s1,s2] in Path_Rel R )
assume A1:
s1 <= s2
; [s1,s2] in Path_Rel R
set p = <*s1,s2*>;
A2:
len <*s1,s2*> = 2
by FINSEQ_1:44;
A3:
<*s1,s2*> . 1 = s1
by FINSEQ_1:44;
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;
( 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*> )
;
( [(<*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 A3, A5, FINSEQ_1:44;
verum
end;
<*s1,s2*> . (len <*s1,s2*>) = s2
by A2, FINSEQ_1:44;
hence
[s1,s2] in Path_Rel R
by A2, A3, A4, Def3; verum