set P = Dir001 ;
take Dir001 ; :: thesis: not Dir001 is zero_proj3
reconsider u = |[0,0,1]| as non zero Element of (TOP-REAL 3) ;

now :: thesis: ( Dir001 = Dir u & u . 3 <> 0 )

thus Dir001 = Dir u ; :: thesis: u . 3 <> 0
|[0,0,1]| = |[(u . 1),(u . 2),(u . 3)]| by EUCLID_8:1, EUCLID_8:def 3;
hence u . 3 <> 0 by FINSEQ_1:78; :: thesis: verum

end;

hence not Dir001 is zero_proj3 ; :: thesis: verum