theorem :: ANALORT:3

for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
Ortm (x,y,(0. V)) = 0. V