:: deftheorem defines # GEOMTRAP:def 11 :
for AMS being non empty AfMidStruct
for a, b being Element of AMS holds a # b = the MIDPOINT of AMS . (a,b);