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

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

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

not b