theorem Th25: :: MODELC_1:25

for S being non empty set
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