let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( not Dir100 , Dir010 ,P are_collinear & not Dir100 , Dir001 ,P are_collinear & not Dir010 , Dir001 ,P are_collinear implies ex a, b, c being non zero Element of F_Real st P = Dir |[a,b,c]| )
assume that
A1: not Dir100 , Dir010 ,P are_collinear and
A2: not Dir100 , Dir001 ,P are_collinear and
A3: not Dir010 , Dir001 ,P are_collinear ; :: thesis: ex a, b, c being non zero Element of F_Real st P = Dir |[a,b,c]|
consider a, b, c being Element of F_Real such that
A4: P = Dir |[a,b,c]| and
A5: ( a <> 0 or b <> 0 or c <> 0 ) by Th22;
( not a is zero & not b is zero & not c is zero ) by A1, A2, A3, A4, A5, Lem07;
then reconsider a = a, b = b, c = c as non zero Element of F_Real ;
take a ; :: thesis: ex b, c being non zero Element of F_Real st P = Dir |[a,b,c]|
take b ; :: thesis: ex c being non zero Element of F_Real st P = Dir |[a,b,c]|
take c ; :: thesis: P = Dir |[a,b,c]|
thus P = Dir |[a,b,c]| by A4; :: thesis: verum