let P be Point of (); :: 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
for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
() . P = Dir111 )

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
for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
() . P = Dir111

consider a, b, c being non zero Element of F_Real such that
A4: P = Dir |[a,b,c]| by Th23, A1, A2, A3;
reconsider ia = 1 / a, ib = 1 / b, ic = 1 / c as Element of F_Real by XREAL_0:def 1;
( not ia is zero & not ib is zero & not ic is zero ) by XCMPLX_1:50;
then reconsider ia = ia, ib = ib, ic = ic as non zero Element of F_Real ;
take ia ; :: thesis: ex b, c being non zero Element of F_Real st
for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
() . P = Dir111

take ib ; :: thesis: ex c being non zero Element of F_Real st
for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,c*>*> holds
() . P = Dir111

take ic ; :: thesis: for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds
() . P = Dir111

thus for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds
() . P = Dir111 by ; :: thesis: verum