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 b1 being Element of (TOP-REAL 3) st b1 = |[c,a,b]| holds
not b1 is zero ; :: thesis: verum