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 (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex t being Element of (OASpace V) 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 (OASpace V) st not a,b // c,d & not a,b // d,c holds
ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )
let a, b, c, d be Element of (OASpace V); :: thesis: ( not a,b // c,d & not a,b // d,c implies ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) )
set S = OASpace V;
assume A2: ( not [[a,b],[c,d]] in the CONGR of (OASpace V) & not [[a,b],[d,c]] in the CONGR of (OASpace V) ) ; :: according to ANALOAF:def 2 :: thesis: ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) )
reconsider a' = a, b' = b, c' = c, d' = d as Element of V ;
( not a',b' // c',d' & not a',b' // d',c' ) by A2, Th33;
then consider t' being VECTOR of V such that
A3: ( ( a',b' // a',t' or a',b' // t',a' ) & ( c',d' // c',t' or c',d' // t',c' ) ) by A1, Th31;
reconsider t = t' as Element of (OASpace V) ;
( ( [[a,b],[a,t]] in the CONGR of (OASpace V) or [[a,b],[t,a]] in the CONGR of (OASpace V) ) & ( [[c,d],[c,t]] in the CONGR of (OASpace V) or [[c,d],[t,c]] in the CONGR of (OASpace V) ) ) by A3, Th33;
then ( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) by Def2;
hence ex t being Element of (OASpace V) st
( ( a,b // a,t or a,b // t,a ) & ( c,d // c,t or c,d // t,c ) ) ; :: thesis: verum