:: deftheorem defines Orte ANALORT:def 2 :
for V being RealLinearSpace
for x, y, u being VECTOR of V holds Orte (x,y,u) = ((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y);