let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V st u <> v holds
PProJ w,y,(u - v),(u - v) <> 0
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v being VECTOR of V st u <> v holds
PProJ w,y,(u - v),(u - v) <> 0 )
assume A1: Gen w,y ; :: thesis: for u, v being VECTOR of V st u <> v holds
PProJ w,y,(u - v),(u - v) <> 0
let u, v be VECTOR of V; :: thesis: ( u <> v implies PProJ w,y,(u - v),(u - v) <> 0 )
assume A2: u <> v ; :: thesis: PProJ w,y,(u - v),(u - v) <> 0
assume PProJ w,y,(u - v),(u - v) = 0 ; :: thesis: contradiction
then u - v,u - v are_Ort_wrt w,y by A1, Th34;
then u - v = 0. V by A1, ANALMETR:15;
hence contradiction by A2, RLVECT_1:35; :: thesis: verum