let V be RealLinearSpace; :: thesis: 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 )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies 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 ) )
assume A1: Gen w,y ; :: thesis: 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 )
let p, q, r be Element of (AMSpace (V,w,y)); :: thesis: ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 )
reconsider u = p, v = q, u1 = r as Element of V ;
consider v2 being VECTOR of V such that
A2: v - u,v2 are_Ort_wrt w,y and
A3: v2 <> 0. V by A1, Th8;
set v1 = u1 + v2;
reconsider r1 = u1 + v2 as Element of (AMSpace (V,w,y)) ;
A4: (u1 + v2) - u1 = v2 + (u1 - u1) by RLVECT_1:def 3
.= v2 + (0. V) by RLVECT_1:15
.= v2 by RLVECT_1:4 ;
then u,v,u1,u1 + v2 are_Ort_wrt w,y by A2;
then A5: p,q _|_ r,r1 by Th21;
r <> r1 by A3, A4, RLVECT_1:15;
hence ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 ) by A5; :: thesis: verum