theorem :: SGRAPH1:32

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