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