take Dir001 ; :: thesis: Dir001 is zero_proj2
reconsider p = |[0,0,1]| as non zero Element of (TOP-REAL 3) ;

now :: thesis: for u being non zero Element of (TOP-REAL 3) st Dir001 = Dir u holds
u . 2 = 0

let u be non zero Element of (TOP-REAL 3); :: thesis: ( Dir001 = Dir u implies u . 2 = 0 )
assume Dir001 = Dir u ; :: thesis: u . 2 = 0
then are_Prop u,p by ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A1: u = a * p by ANPROJ_1:1;
thus u . 2 = a * (p . 2) by A1, RVSUM_1:44
.= a * 0
.= 0 ; :: thesis: verum

end;

hence Dir001 is zero_proj2 ; :: thesis: verum