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
thus u . 3 <> 0 ; :: thesis: verum

end;

hence not Dir001 is zero_proj3 ; :: thesis: verum