per cases ( not P is zero_proj1 or ( P is zero_proj1 & not P is zero_proj2 ) or ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 ) ) by Th37;

suppose not P is zero_proj1 ; :: thesis: ( ( for b₁ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & P is zero_proj1 & not P is zero_proj2 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) ) & ( not P is zero_proj1 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) & ( for b₁, b₂ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual1 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & not P is zero_proj2 & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual2 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual3 P9 ) implies b₁ = b₂ ) ) ) )

then reconsider P9 = P as non zero_proj1 Element of (ProjectiveSpace (TOP-REAL 3)) ;
dual1 P9 is Element of ProjectiveLines real_projective_plane ;
hence ( ( for b₁ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & P is zero_proj1 & not P is zero_proj2 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) ) & ( not P is zero_proj1 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) & ( for b₁, b₂ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual1 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & not P is zero_proj2 & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual2 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual3 P9 ) implies b₁ = b₂ ) ) ) ) ; :: thesis: verum

end;

suppose A1: ( P is zero_proj1 & not P is zero_proj2 ) ; :: thesis: ( ( for b₁ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & P is zero_proj1 & not P is zero_proj2 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) ) & ( not P is zero_proj1 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) & ( for b₁, b₂ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual1 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & not P is zero_proj2 & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual2 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual3 P9 ) implies b₁ = b₂ ) ) ) )

then reconsider P9 = P as non zero_proj2 Element of (ProjectiveSpace (TOP-REAL 3)) ;
dual2 P9 is Element of ProjectiveLines real_projective_plane ;
hence ( ( for b₁ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & P is zero_proj1 & not P is zero_proj2 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) ) & ( not P is zero_proj1 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) & ( for b₁, b₂ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual1 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & not P is zero_proj2 & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual2 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual3 P9 ) implies b₁ = b₂ ) ) ) ) by A1; :: thesis: verum

end;

suppose A3: ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 ) ; :: thesis: ( ( for b₁ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & P is zero_proj1 & not P is zero_proj2 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) ) & ( not P is zero_proj1 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) & ( for b₁, b₂ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual1 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & not P is zero_proj2 & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual2 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual3 P9 ) implies b₁ = b₂ ) ) ) )

then reconsider P9 = P as non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)) ;
dual3 P9 is Element of ProjectiveLines real_projective_plane ;
hence ( ( for b₁ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & P is zero_proj1 & not P is zero_proj2 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) ) & ( not P is zero_proj1 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) & ( for b₁, b₂ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual1 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & not P is zero_proj2 & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual2 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual3 P9 ) implies b₁ = b₂ ) ) ) ) by A3; :: thesis: verum

end;

end;