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

hence
for bassume
|[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;then a = |[0,0,0]| `3 by EUCLID_5:2, EUCLID_5:4;

hence contradiction by EUCLID_5:2; :: thesis: verum

not b