IncProjSp_of real_projective_plane is 2-dimensional

proof

for M, N being LINE of (IncProjSp_of real_projective_plane) ex q being POINT of (IncProjSp_of real_projective_plane) st
( q on M & q on N )

proof

let M, N be LINE of (IncProjSp_of real_projective_plane); :: thesis: ex q being POINT of (IncProjSp_of real_projective_plane) st
( q on M & q on N )
consider p1, q1 being Point of real_projective_plane such that
p1 <> q1 and
A1: M = Line (p1,q1) by Th60;
consider p2, q2 being Point of real_projective_plane such that
p2 <> q2 and
A2: N = Line (p2,q2) by Th60;
consider q being Element of real_projective_plane such that
A3: p1,q1,q are_collinear and
A4: p2,q2,q are_collinear by ANPROJ_2:def 14;
reconsider Q = q as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
take Q ; :: thesis: ( Q on M & Q on N )
thus ( Q on M & Q on N ) by A1, A2, A3, A4, Th61; :: thesis: verum

end;

hence IncProjSp_of real_projective_plane is 2-dimensional by INCPROJ:def 9; :: thesis: verum

end;

hence IncProjSp_of real_projective_plane is IncProjectivePlane ; :: thesis: verum