now :: thesis: not |[b,c,a]| is zero

assume |[b,c,a]| is zero ; :: thesis: contradiction
then a = |[0,0,0]| `3 by EUCLID_5:2, EUCLID_5:4;
hence contradiction by EUCLID_5:2; :: thesis: verum

end;

hence for b₁ being Element of (TOP-REAL 3) st b₁ = |[b,c,a]| holds
not b₁ is zero ; :: thesis: verum