:: deftheorem defines ]. NDIFF_5:def 2 :
for S being RealLinearSpace
for p, q being Point of S holds ].p,q.[ = [.p,q.] \ {p,q};