let V be RealLinearSpace; :: thesis: for u, u1, v, v1 being VECTOR of V holds
( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let u, u1, v, v1 be VECTOR of V; :: thesis: ( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )

A1: now :: thesis: for w, y, w1, y1 being VECTOR of V st ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & a = 0 & b <> 0 ) holds
w,y // w1,y1

let w, y, w1, y1 be VECTOR of V; :: thesis: ( ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & a = 0 & b <> 0 ) implies w,y // w1,y1 )
given a, b being Real such that A2: ( a * (y - w) = b * (y1 - w1) & a = 0 ) and
A3: b <> 0 ; :: thesis: w,y // w1,y1
0. V = b * (y1 - w1) by A2, RLVECT_1:10;
then y1 - w1 = 0. V by A3, RLVECT_1:11;
then y1 = w1 by RLVECT_1:21;
hence w,y // w1,y1 by ANALOAF:9; :: thesis: verum

end;

A4: now :: thesis: for w, y, w1, y1 being VECTOR of V st ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & 0 < a & b < 0 ) holds
w,y // y1,w1

let w, y, w1, y1 be VECTOR of V; :: thesis: ( ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & 0 < a & b < 0 ) implies w,y // y1,w1 )
given a, b being Real such that A5: a * (y - w) = b * (y1 - w1) and
A6: 0 < a and
A7: b < 0 ; :: thesis: w,y // y1,w1
A8: a * (y - w) = b * (- (w1 - y1)) by A5, RLVECT_1:33
.= (- b) * (w1 - y1) by RLVECT_1:24 ;
0 < - b by A7, XREAL_1:58;
hence w,y // y1,w1 by A6, A8, ANALOAF:def 1; :: thesis: verum

end;

A9: now :: thesis: ( for a, b being Real holds
( not a * (v - u) = b * (v1 - u1) or ( not a <> 0 & not b <> 0 ) ) or u,v // u1,v1 or u,v // v1,u1 )

given a, b being Real such that A10: a * (v - u) = b * (v1 - u1) and
A11: ( a <> 0 or b <> 0 ) ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )

A12: now :: thesis: ( a <> 0 & b <> 0 & not u,v // u1,v1 implies u,v // v1,u1 )

A13: now :: thesis: ( a < 0 & b < 0 & not u,v // u1,v1 implies u,v // v1,u1 )

assume ( a < 0 & b < 0 ) ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then A14: ( 0 < - a & 0 < - b ) by XREAL_1:58;
(- a) * (u - v) = a * (- (u - v)) by RLVECT_1:24
.= b * (v1 - u1) by A10, RLVECT_1:33
.= b * (- (u1 - v1)) by RLVECT_1:33
.= (- b) * (u1 - v1) by RLVECT_1:24 ;
then v,u // v1,u1 by A14, ANALOAF:def 1;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; :: thesis: verum

end;

A15: now :: thesis: ( a < 0 & 0 < b & not u,v // u1,v1 implies u,v // v1,u1 )

assume ( a < 0 & 0 < b ) ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then u1,v1 // v,u by A4, A10;
then v,u // u1,v1 by ANALOAF:12;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; :: thesis: verum

end;

assume A16: ( a <> 0 & b <> 0 ) ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )
( 0 < a & b < 0 & not u,v // u1,v1 implies u,v // v1,u1 ) by A4, A10;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by A10, A16, A15, A13, ANALOAF:def 1; :: thesis: verum

end;

now :: thesis: ( not b = 0 or u,v // u1,v1 or u,v // v1,u1 )

assume b = 0 ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then u1,v1 // u,v by A1, A10, A11;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; :: thesis: verum

end;

hence ( u,v // u1,v1 or u,v // v1,u1 ) by A1, A10, A12; :: thesis: verum

end;

A17: now :: thesis: for w, y, w1, y1 being VECTOR of V st w,y // w1,y1 holds
ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )

let w, y, w1, y1 be VECTOR of V; :: thesis: ( w,y // w1,y1 implies ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) )
assume A18: w,y // w1,y1 ; :: thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )

A19: now :: thesis: ( w = y implies ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) )

assume w = y ; :: thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )
then 1 * (y - w) = 0. V by RLVECT_1:10, RLVECT_1:15
.= 0 * (y1 - w1) by RLVECT_1:10 ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ; :: thesis: verum

end;

A20: now :: thesis: ( w1 = y1 implies ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) )

assume w1 = y1 ; :: thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )
then 1 * (y1 - w1) = 0. V by RLVECT_1:10, RLVECT_1:15
.= 0 * (y - w) by RLVECT_1:10 ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ; :: thesis: verum

end;

( ex a, b being Real st
( 0 < a & 0 < b & a * (y - w) = b * (y1 - w1) ) implies ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ) ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) by A18, A19, A20, ANALOAF:def 1; :: thesis: verum

end;

now :: thesis: ( u,v // v1,u1 implies ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )

assume u,v // v1,u1 ; :: thesis: ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) )
then consider a, b being Real such that
A21: a * (v - u) = b * (u1 - v1) and
A22: ( a <> 0 or b <> 0 ) by A17;
A23: ( a <> 0 or - b <> 0 ) by A22;
(- b) * (v1 - u1) = b * (- (v1 - u1)) by RLVECT_1:24
.= a * (v - u) by A21, RLVECT_1:33 ;
hence ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A23; :: thesis: verum

end;

hence ( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) by A17, A9; :: thesis: verum