let S be non empty set ; :: thesis: for R being total Relation of S,S
for s0 being Element of S ex pai being inf_path of R st pai . 0 = s0
let R be total Relation of S,S; :: thesis: for s0 being Element of S ex pai being inf_path of R st pai . 0 = s0
let s0 be Element of S; :: thesis: ex pai being inf_path of R st pai . 0 = s0
consider pai being sequence of S such that
A1: pai . 0 = s0 and
A2: for n being Nat holds [(pai . n),(pai . (n + 1))] in R by Lm33;
reconsider pai = pai as inf_path of R by A2, Def39;
take pai ; :: thesis: pai . 0 = s0
thus pai . 0 = s0 by A1; :: thesis: verum