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

assume |[a,b,c]| is zero ; :: thesis: contradiction
then a = |[0,0,0]| `1 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₁ = |[a,b,c]| holds
not b₁ is zero ; :: thesis: verum