:: deftheorem defines are_homotopic TOPALG_6:def 11 :
for T being non empty TopStruct
for c1, c2 being with_endpoints Curve of T holds
( c1,c2 are_homotopic iff ex a, b being Point of T ex p1, p2 being Path of a,b st
( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic ) );