|[1,0,0]| <> |[0,0,0]|

proof

assume |[1,0,0]| = |[0,0,0]| ; :: thesis: contradiction
then 1 = |[0,0,0]| `1 by EUCLID_5:2;
hence contradiction by EUCLID_5:2; :: thesis: verum

end;

hence <e1> <> 0. (TOP-REAL 3) by EUCLID_5:4, EUCLID_8:def 1; :: thesis: ( <e2> <> 0. (TOP-REAL 3) & <e3> <> 0. (TOP-REAL 3) )
|[0,1,0]| <> |[0,0,0]|

proof

assume |[0,1,0]| = |[0,0,0]| ; :: thesis: contradiction
then 1 = |[0,0,0]| `2 by EUCLID_5:2;
hence contradiction by EUCLID_5:2; :: thesis: verum

end;

hence <e2> <> 0. (TOP-REAL 3) by EUCLID_5:4, EUCLID_8:def 2; :: thesis: <e3> <> 0. (TOP-REAL 3)
|[0,0,1]| <> |[0,0,0]|

proof

assume |[0,0,1]| = |[0,0,0]| ; :: thesis: contradiction
then 1 = |[0,0,0]| `3 by EUCLID_5:2;
hence contradiction by EUCLID_5:2; :: thesis: verum

end;

hence <e3> <> 0. (TOP-REAL 3) by EUCLID_5:4, EUCLID_8:def 3; :: thesis: verum