let V be RealLinearSpace; for w, y being VECTOR of V
for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let w, y be VECTOR of V; for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let p, p1 be Element of (AMSpace (V,w,y)); ( Gen w,y & p <> p1 implies for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q ) )
assume that
A1:
Gen w,y
and
A2:
p <> p1
; for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let q be Element of (AMSpace (V,w,y)); ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
reconsider u = p, v = q, u1 = p1 as Element of V ;
u1 - u <> 0. V
by A2, RLVECT_1:21;
then consider a being Real such that
A3:
(v - u) - (a * (u1 - u)),u1 - u are_Ort_wrt w,y
by A1, Th13;
set v1 = u + (a * (u1 - u));
reconsider q1 = u + (a * (u1 - u)) as Element of (AMSpace (V,w,y)) ;
v - (u + (a * (u1 - u))) = (v - u) - (a * (u1 - u))
by RLVECT_1:27;
then
u1 - u,v - (u + (a * (u1 - u))) are_Ort_wrt w,y
by A3;
then
u,u1,u + (a * (u1 - u)),v are_Ort_wrt w,y
;
then A4:
p,p1 _|_ q1,q
by Th21;
a * (u1 - u) =
(a * (u1 - u)) + (0. V)
by RLVECT_1:4
.=
(a * (u1 - u)) + (u - u)
by RLVECT_1:15
.=
(u + (a * (u1 - u))) - u
by RLVECT_1:def 3
.=
1 * ((u + (a * (u1 - u))) - u)
by RLVECT_1:def 8
;
then
p,p1 // p,q1
by Th22;
hence
ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
by A4; verum