:: deftheorem Def12 defines + TOPALG_6:def 12 :
for T being TopStruct
for c1, c2 being Curve of T holds
( ( c1 \/ c2 is Curve of T implies c1 + c2 = c1 \/ c2 ) & ( c1 \/ c2 is not Curve of T implies c1 + c2 = {} ) );