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 Function of NAT,S such that
A1: pai . 0 = s0 and
A2: for n being Element of NAT holds [(pai . n),(pai . (n + 1))] in R by Lm34;
reconsider pai = pai as inf_path of R by A2, Def41;
take pai ; :: thesis: pai . 0 = s0
thus pai . 0 = s0 by A1; :: thesis: verum