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:
A2: u <> v by A1, Th28;
set S = OASpace V;
thus ex a, b being Element of (OASpace V) st a <> b by A2; :: 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 a' = a, b' = b, c' = c, d' = d, p' = p, q' = q, r' = r, s' = s as Element of V ;
thus [[a,b],[c,c]] in the CONGR of (OASpace V) :: according to ANALOAF:def 2 :: thesis:

a',b' // c',c' by Def1;
hence [[a,b],[c,c]] in the CONGR of (OASpace V) by Th33; :: thesis:

end;

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

assume [[a,b],[b,a]] in the CONGR of (OASpace V) ; :: according to ANALOAF:def 2 :: thesis:
then a',b' // b',a' by Th33;
hence a = b by Th19; :: thesis:

end;

thus ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) :: thesis:

assume ( a <> b & [[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:
then ( a' <> b' & a',b' // p',q' & a',b' // r',s' ) by Th33;
then p',q' // r',s' by Th20;
then [[p,q],[r,s]] in the CONGR of (OASpace V) by Th33;
hence p,q // r,s by Def2; :: 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 a',b' // c',d' by Th33;
then b',a' // d',c' by Th21;
then [[b,a],[d,c]] in the CONGR of (OASpace V) by Th33;
hence b,a // d,c by Def2; :: 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 a',b' // b',c' by Th33;
then a',b' // a',c' by Th22;
then [[a,b],[a,c]] in the CONGR of (OASpace V) by Th33;
hence a,b // a,c by Def2; :: 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 a',b' // a',c' by Th33;
then ( a',b' // b',c' or a',c' // c',b' ) by Th23;
then ( [[a,b],[b,c]] in the CONGR of (OASpace V) or [[a,c],[c,b]] in the CONGR of (OASpace V) ) by Th33;
hence ( a,b // b,c or a,c // c,b ) by Def2; :: 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 a', b', c', d' being VECTOR of V such that
A3: ( not a',b' // c',d' & not a',b' // d',c' ) by A1, Th29;
reconsider a = a', b = b', c = c', d = d' as Element of (OASpace V) ;
( not [[a,b],[c,d]] in the CONGR of (OASpace V) & not [[a,b],[d,c]] in the CONGR of (OASpace V) ) by A3, Th33;
then ( not a,b // c,d & not a,b // d,c ) by Def2;
hence ex a, b, c, d being Element of (OASpace V) st
( not a,b // c,d & not a,b // d,c ) ; :: 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 a' = a, b' = b, c' = c as Element of V ;
consider d' being VECTOR of V such that
A4: ( a',b' // c',d' & a',c' // b',d' & b' <> d' ) by A2, Th26;
reconsider d = d' as Element of (OASpace V) ;
( [[a,b],[c,d]] in the CONGR of (OASpace V) & [[a,c],[b,d]] in the CONGR of (OASpace V) ) by A4, Th33;
then ( a,b // c,d & a,c // b,d & b <> d ) by A4, Def2;
hence ex d being Element of (OASpace V) st
( a,b // c,d & a,c // b,d & b <> d ) ; :: 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 A5: ( p <> b & [[b,p],[p,c]] in the CONGR of (OASpace V) ) ; :: according to ANALOAF:def 2 :: thesis:
reconsider p' = p, a' = a, b' = b, c' = c as Element of V ;
( p' <> b' & b',p' // p',c' ) by A5, Th33;
then consider d' being VECTOR of V such that
A6: ( a',p' // p',d' & a',b' // c',d' ) by Th27;
reconsider d = d' as Element of (OASpace V) ;
( [[a,p],[p,d]] in the CONGR of (OASpace V) & [[a,b],[c,d]] in the CONGR of (OASpace V) ) by A6, Th33;
then ( a,p // p,d & a,b // c,d ) by Def2;
hence ex d being Element of (OASpace V) st
( a,p // p,d & a,b // c,d ) ; :: thesis:

end;