let u, v, w be Point of (TOP-REAL 3); ( 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 )
; |{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
; verum