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 that
A1: not p is zero and
A2: not q is zero ; :: thesis: ( Dir p = Dir q iff are_Prop p,q )
A3: p in NonZero V by A1, STRUCT_0:1;
A4: now :: thesis: ( Dir p = Dir q implies are_Prop p,q )
assume Dir p = Dir q ; :: thesis: are_Prop p,q
then [p,q] in Proportionality_as_EqRel_of V by A3, EQREL_1:35;
hence are_Prop p,q by Th20; :: thesis: verum
end;
now :: thesis: ( are_Prop p,q implies Dir p = Dir q )
assume are_Prop p,q ; :: thesis: Dir p = Dir q
then [p,q] in Proportionality_as_EqRel_of V by A1, A2, Th20;
hence Dir p = Dir q by A3, EQREL_1:35; :: thesis: verum
end;
hence ( Dir p = Dir q iff are_Prop p,q ) by A4; :: thesis: verum