let u, v, w be Point of (TOP-REAL 3); :: thesis: ( ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) & a <> 0 ) implies |{u,v,w}| = 0 )
assume A4: ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) & a <> 0 ) ; :: thesis: |{u,v,w}| = 0
consider a, b, c being Real such that
B1: ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) and
B2: a <> 0 by A4;
reconsider u1 = u, v1 = v, w1 = w as Element of REAL 3 by EUCLID:22;
reconsider vw = v <X> w as Element of REAL 3 by EUCLID:22;
|{u,v,w}| = |{((((- b) / a) * v) + (((- c) / a) * w)),v,w}| by B1, B2, Th10
.= |(((((- b) / a) * v) + (((- c) / a) * w)),(v <X> w))| by EUCLID_5:def 5
.= (((- b) / a) * |(v1,vw)|) + (((- c) / a) * |(w1,vw)|) by EUCLID_4:27
.= (((- b) / a) * |{v,v,w}|) + (((- c) / a) * |(w1,vw)|) by EUCLID_5:def 5
.= (((- b) / a) * |{v,v,w}|) + (((- c) / a) * |{w,v,w}|) by EUCLID_5:def 5
.= (((- b) / a) * 0) + (((- c) / a) * |{w,v,w}|) by EUCLID_5:31
.= (((- b) / a) * 0) + (((- c) / a) * 0) by EUCLID_5:31
.= 0 ;
hence |{u,v,w}| = 0 ; :: thesis: verum