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