let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n st x1 // x2 holds
not x1 _|_ x2
let x1, x2 be Element of REAL n; :: thesis: ( x1 // x2 implies not x1 _|_ x2 )
assume A1: x1 // x2 ; :: thesis: not x1 _|_ x2
then consider r being Real such that
A2: x1 = r * x2 by Def1;
A3: ( x1 <> 0* n & x2 <> 0* n ) by A1, Def1;
then A4: r <> 0 by A2, EUCLID_4:3;
A5: |(x1,x2)| = r * |(x2,x2)| by A2, EUCLID_4:26;
|(x2,x2)| <> 0 by A3, EUCLID_4:22;
then |(x1,x2)| <> 0 by A4, A5, XCMPLX_1:6;
then not x1,x2 are_orthogonal by EUCLID_2:def 3;
hence not x1 _|_ x2 by Def3; :: thesis: verum