let V be non trivial RealLinearSpace; :: thesis: for p, q being Element of V st not p is zero & not q is zero holds
( Dir p = Dir q iff are_Prop p,q )
let p, q be Element of V; :: thesis: ( not p is zero & not q is zero implies ( Dir p = Dir q iff are_Prop p,q ) )
assume A1: ( not p is zero & not q is zero ) ; :: thesis: ( Dir p = Dir q iff are_Prop p,q )
then A2: p in NonZero V by STRUCT_0:1;

A3: now

assume Dir p = Dir q ; :: thesis: are_Prop p,q
then [p,q] in Proportionality_as_EqRel_of V by A2, EQREL_1:44;
hence are_Prop p,q by Th29; :: thesis: verum

end;

now

assume are_Prop p,q ; :: thesis: Dir p = Dir q
then [p,q] in Proportionality_as_EqRel_of V by A1, Th29;
hence Dir p = Dir q by A2, EQREL_1:44; :: thesis: verum

end;

hence ( Dir p = Dir q iff are_Prop p,q ) by A3; :: thesis: verum