let S be non empty set ; :: thesis: for R being total Relation of S,S
for s0, s1 being Element of S st [s0,s1] in R holds
ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 )
let R be total Relation of S,S; :: thesis: for s0, s1 being Element of S st [s0,s1] in R holds
ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 )
let s0, s1 be Element of S; :: thesis: ( [s0,s1] in R implies ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 ) )
consider pai1 being inf_path of R such that
A1: pai1 . 0 = s1 by Th25;
deffunc H₁( object ) -> Element of S = PrePath ($1,s0,pai1);
A2: for x being object st x in NAT holds
H₁(x) in S ;
consider pai being sequence of S such that
A3: for n being object st n in NAT holds
pai . n = H₁(n) from FUNCT_2:sch 2(A2);
assume A4: [s0,s1] in R ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 )
for n being Nat holds [(pai . n),(pai . (n + 1))] in R

proof

let n be Nat; :: thesis: [(pai . n),(pai . (n + 1))] in R
set n1 = n + 1;
set n0 = n - 1;

per cases ( n = 0 or n <> 0 ) ;

suppose A5: n = 0 ; :: thesis: [(pai . n),(pai . (n + 1))] in R

then A6: k_nat ((k_nat (n + 1)) - 1) = k_nat (1 - 1) by Def2
.= 0 by Def2 ;
A7: pai . n = H₁(n) by A3, A5
.= s0 by A5, Def61 ;
pai . (n + 1) = H₁(n + 1) by A3
.= s1 by A1, A6, Def61 ;
hence [(pai . n),(pai . (n + 1))] in R by A4, A7; :: thesis: verum

end;

suppose A8: n <> 0 ; :: thesis: [(pai . n),(pai . (n + 1))] in R

then reconsider n0 = n - 1 as Element of NAT by NAT_1:20;
A9: pai . (n + 1) = H₁(n + 1) by A3
.= pai1 . (k_nat ((k_nat (n + 1)) - 1)) by Def61
.= pai1 . (k_nat ((n + 1) - 1)) by Def2
.= pai1 . (n0 + 1) by Def2 ;
A10: n in NAT by ORDINAL1:def 12;
then pai . n = H₁(n) by A3
.= pai1 . (k_nat ((k_nat n) - 1)) by A8, Def61
.= pai1 . (k_nat (n - 1)) by Def2, A10
.= pai1 . n0 by Def2 ;
hence [(pai . n),(pai . (n + 1))] in R by A9, Def39; :: thesis: verum

end;

end;

end;

then reconsider pai = pai as inf_path of R by Def39;
A11: pai . 0 = H₁( 0 ) by A3
.= s0 by Def61 ;
take pai ; :: thesis: ( pai . 0 = s0 & pai . 1 = s1 )
pai . 1 = H₁(1) by A3
.= pai1 . (k_nat ((k_nat 1) - 1)) by Def61
.= pai1 . (k_nat (1 - 1)) by Def2
.= s1 by A1, Def2 ;
hence ( pai . 0 = s0 & pai . 1 = s1 ) by A11; :: thesis: verum