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;

( 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;then [p,q] in Proportionality_as_EqRel_of V by A3, EQREL_1:35;

hence are_Prop p,q by Th20; :: thesis: verum

now :: thesis: ( are_Prop p,q implies Dir p = Dir q )

hence
( Dir p = Dir q iff are_Prop p,q )
by A4; :: thesis: verumassume
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;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