:: deftheorem defines Loops TOPALG_1:def 2 :
for T being non empty TopStruct
for t being Point of T holds Loops t = Paths (t,t);