Graphical definition of the finite

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