:: deftheorem Def1 defines Paths TOPALG_1:def 1 :
for T being non empty TopStruct
for t1, t2 being Point of T
for b₄ being set holds
( b₄ = Paths (t1,t2) iff for x being object holds
( x in b₄ iff x is Path of t1,t2 ) );