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);
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
;
( Q on M & Q on N )
thus
(
Q on M &
Q on N )
by A1, A2, A3, A4, Th61;
verum
end;
hence
IncProjSp_of real_projective_plane is
2-dimensional
by INCPROJ:def 9;
verum
end;
hence
IncProjSp_of real_projective_plane is IncProjectivePlane
; verum