let S be non empty set ; :: thesis: for R being total Relation of S,S
for s0 being Element of S ex f being sequence of S st
( f . 0 = s0 & ( for n being Nat holds [(f . n),(f . (n + 1))] in R ) )
let R be total Relation of S,S; :: thesis: for s0 being Element of S ex f being sequence of S st
( f . 0 = s0 & ( for n being Nat holds [(f . n),(f . (n + 1))] in R ) )
let s0 be Element of S; :: thesis: ex f being sequence of S st
( f . 0 = s0 & ( for n being Nat holds [(f . n),(f . (n + 1))] in R ) )
deffunc H₁( Element of S) -> non empty set = S;
A1: for s being Element of S holds (Im (R,s)) /\ H₁(s) is non empty Subset of S

proof

let s be Element of S; :: thesis: (Im (R,s)) /\ H₁(s) is non empty Subset of S
set X = R .: {s};
A2: rng R c= S by RELAT_1:def 19;
A3: R .: {s} c= rng R by RELAT_1:111;
then (R .: {s}) /\ H₁(s) = R .: {s} by A2, XBOOLE_1:1, XBOOLE_1:28;
hence (Im (R,s)) /\ H₁(s) is non empty Subset of S by A3, A2, Lm32, XBOOLE_1:1; :: thesis: verum

end;

consider f being sequence of S such that
A4: ( f . 0 = s0 & ( for n being Element of NAT holds
( [(f . n),(f . (n + 1))] in R & f . (n + 1) in H₁(f . n) ) ) ) from MODELC_1:sch 1(A1);
take f ; :: thesis: ( f . 0 = s0 & ( for n being Nat holds [(f . n),(f . (n + 1))] in R ) )
thus f . 0 = s0 by A4; :: thesis: for n being Nat holds [(f . n),(f . (n + 1))] in R
let n be Nat; :: thesis: [(f . n),(f . (n + 1))] in R
n in NAT by ORDINAL1:def 12;
hence [(f . n),(f . (n + 1))] in R by A4; :: thesis: verum