:: deftheorem defines PATHS SGRAPH1:def 10 :
for X being set
for g being SimpleGraph of X
for v1, v2 being Element of the carrier of g holds PATHS (v1,v2) = { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;