let V be RealLinearSpace; :: thesis: for v, w being Point of V st 0. V in LSeg v,w holds
ex r being Real st
( v = r * w or w = r * v )
let v, w be Point of V; :: thesis: ( 0. V in LSeg v,w implies ex r being Real st
( v = r * w or w = r * v ) )
assume 0. V in LSeg v,w ; :: thesis: ex r being Real st
( v = r * w or w = r * v )
then consider s being Real such that
A2: 0. V = ((1 - s) * v) + (s * w) and
( 0 <= s & s <= 1 ) ;
- (s * w) = (1 - s) * v by A2, RLVECT_1:19;
then A3: (- s) * w = (1 - s) * v by RLVECT_1:98;

per cases ( - s <> 0 or - s = 0 ) ;

suppose A4: - s <> 0 ; :: thesis: ex r being Real st
( v = r * w or w = r * v )

take r = ((- s) " ) * (1 - s); :: thesis: ( v = r * w or w = r * v )
w = 1 * w by RLVECT_1:def 9
.= (((- s) " ) * (- s)) * w by A4, XCMPLX_0:def 7
.= ((- s) " ) * ((- s) * w) by RLVECT_1:def 9
.= r * v by A3, RLVECT_1:def 9 ;
hence ( v = r * w or w = r * v ) ; :: thesis: verum

end;

suppose S: - s = 0 ; :: thesis: ex r being Real st
( v = r * w or w = r * v )

take - s ; :: thesis: ( v = (- s) * w or w = (- s) * v )
thus ( v = (- s) * w or w = (- s) * v ) by A3, S, RLVECT_1:def 9; :: thesis: verum

end;

end;