let P be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( not P is zero_proj1 or not P is zero_proj2 or not P is zero_proj3 )
assume that
A1: P is zero_proj1 and
A2: P is zero_proj2 and
A3: P is zero_proj3 ; :: thesis: contradiction
consider u being Element of (TOP-REAL 3) such that
A4: not u is zero and
A5: Dir u = P by ANPROJ_1:26;
reconsider u = u as non zero Element of (TOP-REAL 3) by A4;
( u `1 = 0 & u `2 = 0 & u `3 = 0 ) by A1, A2, A3, A5;
hence contradiction by EUCLID_5:3, EUCLID_5:4; :: thesis: verum