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

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

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

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

proof

hence
|[1,0,0]| <> 0. (TOP-REAL 3)
by EUCLID_5:4; :: thesis: ( |[0,1,0]| <> 0. (TOP-REAL 3) & |[0,0,1]| <> 0. (TOP-REAL 3) & |[1,1,1]| <> 0. (TOP-REAL 3) )
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;then 1 = |[0,0,0]| `1 by EUCLID_5:2;

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

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

proof

hence
|[0,1,0]| <> 0. (TOP-REAL 3)
by EUCLID_5:4; :: thesis: ( |[0,0,1]| <> 0. (TOP-REAL 3) & |[1,1,1]| <> 0. (TOP-REAL 3) )
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;then 1 = |[0,0,0]| `2 by EUCLID_5:2;

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

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

proof

hence
|[0,0,1]| <> 0. (TOP-REAL 3)
by EUCLID_5:4; :: thesis: |[1,1,1]| <> 0. (TOP-REAL 3)
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;then 1 = |[0,0,0]| `3 by EUCLID_5:2;

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

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

proof

hence
|[1,1,1]| <> 0. (TOP-REAL 3)
by EUCLID_5:4; :: thesis: verum
assume
|[1,1,1]| = |[0,0,0]|
; :: thesis: contradiction

then 1 = |[0,0,0]| `1 by EUCLID_5:2;

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

end;then 1 = |[0,0,0]| `1 by EUCLID_5:2;

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