let p, q be Point of (TOP-REAL 2); :: thesis: for r being Real st p `1 = q `2 & - (p `2) = q `1 & p = r * q holds
( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) )
let r be Real; :: thesis: ( p `1 = q `2 & - (p `2) = q `1 & p = r * q implies ( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) ) )
A1: 1 + (r * r) > 0 + 0 by XREAL_1:8, XREAL_1:63;
assume ( p `1 = q `2 & - (p `2) = q `1 & p = r * q ) ; :: thesis: ( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) )
then A2: p = |[(r * (- (p `2))),(r * (p `1))]| by EUCLID:57;
then p `2 = r * (p `1) ;
then p `1 = - (r * (r * (p `1))) by A2
.= - ((r * r) * (p `1)) ;
then (1 + (r * r)) * (p `1) = 0 ;
hence A3: p `1 = 0 by A1, XCMPLX_1:6; :: thesis: ( p `2 = 0 & p = 0. (TOP-REAL 2) )
p `1 = r * (- (p `2)) by A2;
then p `2 = - ((r * r) * (p `2)) by A2;
then (1 + (r * r)) * (p `2) = 0 ;
hence p `2 = 0 by A1, XCMPLX_1:6; :: thesis: p = 0. (TOP-REAL 2)
hence p = 0. (TOP-REAL 2) by A3, EUCLID:53, EUCLID:54; :: thesis: verum