:: deftheorem defines .|. BHSP_1:def 1 :
for X being non empty UNITSTR
for x, y being Point of X holds x .|. y = the scalar of X . [x,y];