Define: Define:
P is a path on S⟺∀m∈P[∃k,l∈S[m=(k,l)]]∧
∀y∈S[∃k[(y,k)∈P∨(k,y)∈P]]∧
∀s[∃k((s,k)∈P)⟹∃!k((s,k)∈P)]∧
∀s[∃k((k,s)∈P)⟹∃!k((k,s)∈P)]∧
∃z∀s([∃k((s,k)∈P)∧∃r((r,s)∈P)]⟹s=z)
∧∃z∀s([∃k((k,s)∈P)∧∃r((s,r)∈P)]⟹s=z)
Define: P is a path⟺∃S(P is a path on S)
Define: x is a point on P⟺∃S(P is a path on S∧x∈S)
Define: x is an end point on P⟺
x is a point on P∧∃!m∈P(∃k[m=(x,k)]∨∃l[m=(l,x)])
Define: P is an endless path on S⟺
P is a path on S∧∄x(x is an end point on P)
Define: Q subpath P⟺P is a path ∧Q is a path ∧Q⊂P
Define: P is a continuous path⟺P is a path ∧
∀Q,T,A,B(Q≠∅∧T≠∅∧Q is a path on A∧T is a path on B∧Q disjoint T∧(Q∪T) subpath P⟹¬(A disjoint B)
Define: P is a cyclic path on S⟺P is an endlesss path on S ∧
P is a continuous path