let V be RealLinearSpace; :: thesis:
given u, v being VECTOR of V such that A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ; :: thesis:
set S = OASpace V;
A2: u <> v by A1, Th19;
hence ex a, b being Element of (OASpace V) st a <> b ; :: thesis:
thus for a, b, c, d, p, q, r, s being Element of (OASpace V) holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) :: thesis:

let a, b, c, d, p, q, r, s be Element of (OASpace V); :: thesis:
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q, r9 = r, s9 = s as Element of V ;
a9,b9 // c9,c9 ;
hence [[a,b],[c,c]] in the CONGR of (OASpace V) by Def3; :: according to ANALOAF:def 2 :: thesis:
thus ( a,b // b,a implies a = b ) by Th22, Th10; :: thesis:
thus ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) :: thesis:

assume that
A3: a <> b and
A4: ( [[a,b],[p,q]] in the CONGR of (OASpace V) & [[a,b],[r,s]] in the CONGR of (OASpace V) ) ; :: according to ANALOAF:def 2 :: thesis:
( a9,b9 // p9,q9 & a9,b9 // r9,s9 ) by A4, Th22;
then p9,q9 // r9,s9 by A3, Th11;
then [[p,q],[r,s]] in the CONGR of (OASpace V) by Th22;
hence p,q // r,s ; :: thesis:

end;

thus ( a,b // c,d implies b,a // d,c ) :: thesis:

assume [[a,b],[c,d]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def 2 :: thesis:
then a9,b9 // c9,d9 by Th22;
then b9,a9 // d9,c9 by Th12;
then [[b,a],[d,c]] in the CONGR of (OASpace V) by Th22;
hence b,a // d,c ; :: thesis:

end;

thus ( a,b // b,c implies a,b // a,c ) :: thesis:

assume [[a,b],[b,c]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def 2 :: thesis:
then a9,b9 // b9,c9 by Th22;
then a9,b9 // a9,c9 by Th13;
then [[a,b],[a,c]] in the CONGR of (OASpace V) by Th22;
hence a,b // a,c ; :: thesis:

end;

thus ( not a,b // a,c or a,b // b,c or a,c // c,b ) :: thesis:

assume [[a,b],[a,c]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def 2 :: thesis:
then a9,b9 // a9,c9 by Th22;
then ( a9,b9 // b9,c9 or a9,c9 // c9,b9 ) by Th14;
then ( [[a,b],[b,c]] in the CONGR of (OASpace V) or [[a,c],[c,b]] in the CONGR of (OASpace V) ) by Th22;
hence ( a,b // b,c or a,c // c,b ) ; :: thesis:

end;

thus ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) :: thesis:

consider a9, b9, c9, d9 being VECTOR of V such that
A5: not a9,b9 // c9,d9 and
A6: not a9,b9 // d9,c9 by A1, Th20;
reconsider a = a9, b = b9, c = c9, d = d9 as Element of (OASpace V) ;
not [[a,b],[d,c]] in the CONGR of (OASpace V) by A6, Th22;
then A7: not a,b // d,c ;
not [[a,b],[c,d]] in the CONGR of (OASpace V) by A5, Th22;
then not a,b // c,d ;
hence ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) by A7; :: thesis:

end;

thus for a, b, c being Element of (OASpace V) ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) :: thesis:

let a, b, c be Element of (OASpace V); :: thesis:
reconsider a9 = a, b9 = b, c9 = c as Element of V ;
consider d9 being VECTOR of V such that
A8: a9,b9 // c9,d9 and
A9: a9,c9 // b9,d9 and
A10: b9 <> d9 by A2, Th17;
reconsider d = d9 as Element of (OASpace V) ;
[[a,c],[b,d]] in the CONGR of (OASpace V) by A9, Th22;
then A11: a,c // b,d ;
[[a,b],[c,d]] in the CONGR of (OASpace V) by A8, Th22;
then a,b // c,d ;
hence ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) by A10, A11; :: thesis:

end;

thus for p, a, b, c being Element of (OASpace V) st p <> b & b,p // p,c holds
ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) :: thesis:

let p, a, b, c be Element of (OASpace V); :: thesis:
assume that
A12: p <> b and
A13: [[b,p],[p,c]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def 2 :: thesis:
reconsider p9 = p, a9 = a, b9 = b, c9 = c as Element of V ;
b9,p9 // p9,c9 by A13, Th22;
then consider d9 being VECTOR of V such that
A14: a9,p9 // p9,d9 and
A15: a9,b9 // c9,d9 by A12, Th18;
reconsider d = d9 as Element of (OASpace V) ;
[[a,b],[c,d]] in the CONGR of (OASpace V) by A15, Th22;
then A16: a,b // c,d ;
[[a,p],[p,d]] in the CONGR of (OASpace V) by A14, Th22;
then a,p // p,d ;
hence ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) by A16; :: thesis:

end;