let a, b, c be Element of F_Real; :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3)) st P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) holds
( ( not Dir100 , Dir010 ,P are_collinear implies c <> 0 ) & ( not Dir100 , Dir001 ,P are_collinear implies b <> 0 ) & ( not Dir010 , Dir001 ,P are_collinear implies a <> 0 ) )
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) implies ( ( not Dir100 , Dir010 ,P are_collinear implies c <> 0 ) & ( not Dir100 , Dir001 ,P are_collinear implies b <> 0 ) & ( not Dir010 , Dir001 ,P are_collinear implies a <> 0 ) ) )
assume that
A1: P = Dir |[a,b,c]| and
A2: ( a <> 0 or b <> 0 or c <> 0 ) ; :: thesis: ( ( not Dir100 , Dir010 ,P are_collinear implies c <> 0 ) & ( not Dir100 , Dir001 ,P are_collinear implies b <> 0 ) & ( not Dir010 , Dir001 ,P are_collinear implies a <> 0 ) )
thus ( not Dir100 , Dir010 ,P are_collinear implies c <> 0 ) :: thesis: ( ( not Dir100 , Dir001 ,P are_collinear implies b <> 0 ) & ( not Dir010 , Dir001 ,P are_collinear implies a <> 0 ) )

proof

assume A3: not Dir100 , Dir010 ,P are_collinear ; :: thesis: c <> 0
assume A4: c = 0 ; :: thesis: contradiction
A5: not |[a,b,c]| is zero by A2, EUCLID_5:4, FINSEQ_1:78;
A6: not |[1,0,0]|,|[0,1,0]|,|[a,b,c]| are_LinDep by A3, ANPROJ_2:23, Th11, A5, A1;
(((- a) * |[1,0,0]|) + ((- b) * |[0,1,0]|)) + (1 * |[a,b,c]|) = (|[((- a) * 1),((- a) * 0),((- a) * 0)]| + ((- b) * |[0,1,0]|)) + (1 * |[a,b,c]|) by EUCLID_5:8
.= (|[(- a),0,0]| + |[((- b) * 0),((- b) * 1),((- b) * 0)]|) + (1 * |[a,b,c]|) by EUCLID_5:8
.= (|[(- a),0,0]| + |[0,(- b),0]|) + |[(1 * a),(1 * b),(1 * c)]| by EUCLID_5:8
.= |[((- a) + 0),(0 + (- b)),(0 + 0)]| + |[a,b,c]| by EUCLID_5:6
.= |[((- a) + a),((- b) + b),(0 + c)]| by EUCLID_5:6
.= 0. (TOP-REAL 3) by A4, EUCLID_5:4 ;
hence contradiction by A6, ANPROJ_1:def 2; :: thesis: verum

end;

thus ( not Dir100 , Dir001 ,P are_collinear implies b <> 0 ) :: thesis: ( not Dir010 , Dir001 ,P are_collinear implies a <> 0 )

proof

assume A7: not Dir100 , Dir001 ,P are_collinear ; :: thesis: b <> 0
assume A8: b = 0 ; :: thesis: contradiction
A9: not |[a,b,c]| is zero by A2, EUCLID_5:4, FINSEQ_1:78;
A10: not |[1,0,0]|,|[0,0,1]|,|[a,b,c]| are_LinDep by A7, ANPROJ_2:23, Th11, A9, A1;
(((- a) * |[1,0,0]|) + ((- c) * |[0,0,1]|)) + (1 * |[a,b,c]|) = (|[((- a) * 1),((- a) * 0),((- a) * 0)]| + ((- c) * |[0,0,1]|)) + (1 * |[a,b,c]|) by EUCLID_5:8
.= (|[(- a),0,0]| + |[((- c) * 0),((- c) * 0),((- c) * 1)]|) + (1 * |[a,b,c]|) by EUCLID_5:8
.= (|[(- a),0,0]| + |[0,0,(- c)]|) + |[(1 * a),(1 * b),(1 * c)]| by EUCLID_5:8
.= |[((- a) + 0),(0 + 0),(0 + (- c))]| + |[a,b,c]| by EUCLID_5:6
.= |[((- a) + a),(0 + b),((- c) + c)]| by EUCLID_5:6
.= 0. (TOP-REAL 3) by A8, EUCLID_5:4 ;
hence contradiction by A10, ANPROJ_1:def 2; :: thesis: verum

end;

thus ( not Dir010 , Dir001 ,P are_collinear implies a <> 0 ) :: thesis: verum

proof

assume A11: not Dir010 , Dir001 ,P are_collinear ; :: thesis: a <> 0
assume A12: a = 0 ; :: thesis: contradiction
A13: not |[a,b,c]| is zero by A2, EUCLID_5:4, FINSEQ_1:78;
A14: not |[0,1,0]|,|[0,0,1]|,|[a,b,c]| are_LinDep by A11, ANPROJ_2:23, Th11, A13, A1;
(((- b) * |[0,1,0]|) + ((- c) * |[0,0,1]|)) + (1 * |[a,b,c]|) = (|[((- b) * 0),((- b) * 1),((- b) * 0)]| + ((- c) * |[0,0,1]|)) + (1 * |[a,b,c]|) by EUCLID_5:8
.= (|[0,(- b),0]| + |[((- c) * 0),((- c) * 0),((- c) * 1)]|) + (1 * |[a,b,c]|) by EUCLID_5:8
.= (|[0,(- b),0]| + |[0,0,(- c)]|) + |[(1 * a),(1 * b),(1 * c)]| by EUCLID_5:8
.= |[(0 + 0),((- b) + 0),(0 + (- c))]| + |[a,b,c]| by EUCLID_5:6
.= |[(0 + a),((- b) + b),((- c) + c)]| by EUCLID_5:6
.= 0. (TOP-REAL 3) by A12, EUCLID_5:4 ;
hence contradiction by A14, ANPROJ_1:def 2; :: thesis: verum

end;