let a, b, c be Real; for p, q, r being Point of (TOP-REAL 3) st ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) holds
|{p,q,r}| = 0
let p, q, r be Point of (TOP-REAL 3); ( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) implies |{p,q,r}| = 0 )
assume
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) )
; |{p,q,r}| = 0
then consider a, b, c being Real such that
A1:
((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3)
and
A2:
( a <> 0 or b <> 0 or c <> 0 )
;