:: deftheorem defines the_first_point_of TOPALG_6:def 9 :
for T being non empty TopStruct
for c being with_first_point Curve of T holds the_first_point_of c = c . (inf (dom c));