let V be RealLinearSpace; :: thesis: ( ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w implies for a, b, c, d being Element of () st not a,b // c,d & not a,b // d,c holds
ex t being Element of () st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) )

assume A1: ex p, q being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w ; :: thesis: for a, b, c, d being Element of () st not a,b // c,d & not a,b // d,c holds
ex t being Element of () st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )

set S = OASpace V;
let a, b, c, d be Element of (); :: thesis: ( not a,b // c,d & not a,b // d,c implies ex t being Element of () st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) )

reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of V ;
assume ( not [[a,b],[c,d]] in the CONGR of () & not [[a,b],[d,c]] in the CONGR of () ) ; :: according to ANALOAF:def 2 :: thesis: ex t being Element of () st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )

then ( not a9,b9 // c9,d9 & not a9,b9 // d9,c9 ) by Th22;
then consider t9 being VECTOR of V such that
A2: ( a9,b9 // a9,t9 or a9,b9 // t9,a9 ) and
A3: ( c9,d9 // c9,t9 or c9,d9 // t9,c9 ) by ;
reconsider t = t9 as Element of () ;
( [[c,d],[c,t]] in the CONGR of () or [[c,d],[t,c]] in the CONGR of () ) by ;
then A4: ( c,d // c,t or c,d // t,c ) ;
( [[a,b],[a,t]] in the CONGR of () or [[a,b],[t,a]] in the CONGR of () ) by ;
then ( a,b // a,t or a,b // t,a ) ;
hence ex t being Element of () st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) by A4; :: thesis: verum