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

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