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₁( set ) -> Element of S = PrePath ($1,s0,pai1);
A2: for x being set st x in NAT holds
H₁(x) in S ;
consider pai being Function of NAT,S such that
A3: for n being set 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 Element of NAT holds [(pai . n),(pai . (n + 1))] in R

proof

let n be Element of 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
.= s0 by A5, Def63 ;
pai . (n + 1) = H₁(n + 1) by A3
.= s1 by A1, A6, Def63 ;
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 Def63
.= pai1 . (k_nat ((n + 1) - 1)) by Def2
.= pai1 . (n0 + 1) by Def2 ;
pai . n = H₁(n) by A3
.= pai1 . (k_nat ((k_nat n) - 1)) by A8, Def63
.= pai1 . (k_nat (n - 1)) by Def2
.= pai1 . n0 by Def2 ;
hence [(pai . n),(pai . (n + 1))] in R by A9, Def41; :: thesis: verum

end;

end;

end;

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