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

now :: thesis: ( Dir100 = Dir u & u . 1 <> 0 )

thus Dir100 = Dir u ; :: thesis: u . 1 <> 0
thus u . 1 <> 0 ; :: thesis: verum

end;

hence not Dir100 is zero_proj1 ; :: thesis: verum