let V be RealLinearSpace; :: thesis: ( ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) implies ( ex a, b being Element of () st a <> b & ( for a, b, c, d, p, q, r, s being Element of () 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 ) ) ) & ex a, b, c, d being Element of () st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of () ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d ) ) ) )

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: ( ex a, b being Element of () st a <> b & ( for a, b, c, d, p, q, r, s being Element of () 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 ) ) ) & ex a, b, c, d being Element of () st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of () ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d ) ) )

set S = OASpace V;
A2: u <> v by ;
hence ex a, b being Element of () st a <> b ; :: thesis: ( ( for a, b, c, d, p, q, r, s being Element of () 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 ) ) ) & ex a, b, c, d being Element of () st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of () ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d ) ) )

thus for a, b, c, d, p, q, r, s being Element of () 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: ( ex a, b, c, d being Element of () st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of () ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d ) ) )
proof
let a, b, c, d, p, q, r, s be Element of (); :: thesis: ( 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 ) )
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 () by Def3; :: according to ANALOAF:def 2 :: thesis: ( ( 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 ) )
thus ( a,b // b,a implies a = b ) by ; :: thesis: ( ( 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 ) )
thus ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) :: thesis: ( ( 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 ) )
proof
assume that
A3: a <> b and
A4: ( [[a,b],[p,q]] in the CONGR of () & [[a,b],[r,s]] in the CONGR of () ) ; :: according to ANALOAF:def 2 :: thesis: p,q // r,s
( a9,b9 // p9,q9 & a9,b9 // r9,s9 ) by ;
then p9,q9 // r9,s9 by ;
then [[p,q],[r,s]] in the CONGR of () by Th22;
hence p,q // r,s ; :: thesis: verum
end;
thus ( a,b // c,d implies b,a // d,c ) :: thesis: ( ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) )
proof
assume [[a,b],[c,d]] in the CONGR of () ; :: according to ANALOAF:def 2 :: thesis: b,a // d,c
then a9,b9 // c9,d9 by Th22;
then b9,a9 // d9,c9 by Th12;
then [[b,a],[d,c]] in the CONGR of () by Th22;
hence b,a // d,c ; :: thesis: verum
end;
thus ( a,b // b,c implies a,b // a,c ) :: thesis: ( not a,b // a,c or a,b // b,c or a,c // c,b )
proof
assume [[a,b],[b,c]] in the CONGR of () ; :: according to ANALOAF:def 2 :: thesis: a,b // a,c
then a9,b9 // b9,c9 by Th22;
then a9,b9 // a9,c9 by Th13;
then [[a,b],[a,c]] in the CONGR of () by Th22;
hence a,b // a,c ; :: thesis: verum
end;
thus ( not a,b // a,c or a,b // b,c or a,c // c,b ) :: thesis: verum
proof
assume [[a,b],[a,c]] in the CONGR of () ; :: according to ANALOAF:def 2 :: thesis: ( a,b // b,c or a,c // c,b )
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 () or [[a,c],[c,b]] in the CONGR of () ) by Th22;
hence ( a,b // b,c or a,c // c,b ) ; :: thesis: verum
end;
end;
thus ex a, b, c, d being Element of () st
( not a,b // c,d & not a,b // d,c ) :: thesis: ( ( for a, b, c being Element of () ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) ) & ( for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d ) ) )
proof
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 ;
reconsider a = a9, b = b9, c = c9, d = d9 as Element of () ;
not [[a,b],[d,c]] in the CONGR of () by ;
then A7: not a,b // d,c ;
not [[a,b],[c,d]] in the CONGR of () by ;
then not a,b // c,d ;
hence ex a, b, c, d being Element of () st
( not a,b // c,d & not a,b // d,c ) by A7; :: thesis: verum
end;
thus for a, b, c being Element of () ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) :: thesis: for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d )
proof
let a, b, c be Element of (); :: thesis: ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d )

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 ;
reconsider d = d9 as Element of () ;
[[a,c],[b,d]] in the CONGR of () by ;
then A11: a,c // b,d ;
[[a,b],[c,d]] in the CONGR of () by ;
then a,b // c,d ;
hence ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) by ; :: thesis: verum
end;
thus for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d ) :: thesis: verum
proof
let p, a, b, c be Element of (); :: thesis: ( p <> b & b,p // p,c implies ex d being Element of () st
( a,p // p,d & a,b // c,d ) )

assume that
A12: p <> b and
A13: [[b,p],[p,c]] in the CONGR of () ; :: according to ANALOAF:def 2 :: thesis: ex d being Element of () st
( a,p // p,d & a,b // c,d )

reconsider p9 = p, a9 = a, b9 = b, c9 = c as Element of V ;
b9,p9 // p9,c9 by ;
then consider d9 being VECTOR of V such that
A14: a9,p9 // p9,d9 and
A15: a9,b9 // c9,d9 by ;
reconsider d = d9 as Element of () ;
[[a,b],[c,d]] in the CONGR of () by ;
then A16: a,b // c,d ;
[[a,p],[p,d]] in the CONGR of () by ;
then a,p // p,d ;
hence ex d being Element of () st
( a,p // p,d & a,b // c,d ) by A16; :: thesis: verum
end;