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

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