:: deftheorem Def6 defines with_first_point TOPALG_6:def 6 :
for T being TopStruct
for c being Curve of T holds
( c is with_first_point iff dom c is left_end );