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
|[0,1,0]| = |[(u . 1),(u . 2),(u . 3)]| by EUCLID_8:1, EUCLID_8:def 2;
hence u . 2 <> 0 by FINSEQ_1:78; :: thesis: verum
end;
hence not Dir010 is zero_proj2 ; :: thesis: verum