:: deftheorem Def7 defines with_last_point TOPALG_6:def 7 :
for T being TopStruct
for c being Curve of T holds
( c is with_last_point iff dom c is right_end );