let R be POINT of (IncProjSp_of real_projective_plane); :: thesis: for L being LINE of (IncProjSp_of real_projective_plane)
for p, q, r being Point of real_projective_plane st R = r & L = Line (p,q) holds
( R on L iff p,q,r are_collinear )
let L be LINE of (IncProjSp_of real_projective_plane); :: thesis: for p, q, r being Point of real_projective_plane st R = r & L = Line (p,q) holds
( R on L iff p,q,r are_collinear )
let p, q, r be Point of real_projective_plane; :: thesis: ( R = r & L = Line (p,q) implies ( R on L iff p,q,r are_collinear ) )
assume A1: ( R = r & L = Line (p,q) ) ; :: thesis: ( R on L iff p,q,r are_collinear )
hereby :: thesis: ( p,q,r are_collinear implies R on L )
assume R on L ; :: thesis: p,q,r are_collinear
then [R,L] in the Inc of (IncProjSp_of real_projective_plane) by INCSP_1:def 1;
then [R,L] in Proj_Inc real_projective_plane by INCPROJ:2;
then ( R in the carrier of real_projective_plane & L in ProjectiveLines real_projective_plane & ex Y being set st
( L = Y & R in Y ) ) by INCPROJ:def 2;
hence p,q,r are_collinear by A1, COLLSP:11; :: thesis: verum
end;
assume A2: p,q,r are_collinear ; :: thesis: R on L
now :: thesis: ( R in the carrier of real_projective_plane & L in ProjectiveLines real_projective_plane & ex Y being set st
( L = Y & R in Y ) )
R is Point of real_projective_plane by INCPROJ:3;
hence R in the carrier of real_projective_plane ; :: thesis: ( L in ProjectiveLines real_projective_plane & ex Y being set st
( L = Y & R in Y ) )
L is Element of ProjectiveLines real_projective_plane by INCPROJ:1, INCPROJ:4;
hence L in ProjectiveLines real_projective_plane ; :: thesis: ex Y being set st
( L = Y & R in Y )
thus ex Y being set st
( L = Y & R in Y ) by A2, A1, COLLSP:11; :: thesis: verum
end;
then [R,L] in Proj_Inc real_projective_plane by INCPROJ:def 2;
then [R,L] in the Inc of (IncProjSp_of real_projective_plane) by INCPROJ:2;
hence R on L by INCSP_1:def 1; :: thesis: verum