theorem Th27: :: ANALMETR:27

for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for p, q, r being Element of (AMSpace (V,w,y)) ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 )