theorem Th24: :: ANALMETR:24

for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p,q _|_ q1,p1