for X being set
for g being SimpleGraph of X
for v1, v2 being Element of the carrier of g
for e being Element of the carrier of g * st e is_path_of v1,v2 holds
e in PATHS (v1,v2) ;