:: deftheorem defines Mid DIRAF:def 3 :
for S being non empty AffinStruct
for a, b, c being Element of S holds
( Mid a,b,c iff a,b // b,c );