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

now :: thesis: ( Dir010 = Dir u & u . 2 <> 0 )

thus Dir010 = Dir u ; :: thesis: u . 2 <> 0
thus u . 2 <> 0 ; :: thesis: verum

end;

hence not Dir010 is zero_proj2 ; :: thesis: verum