let L1, L2 be LINE of real_projective_plane ; :: thesis: L1 meets L2
reconsider LI1 = L1, LI2 = L2 as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;
consider R being POINT of (IncProjSp_of real_projective_plane) such that
A1: R on LI1 and
A2: R on LI2 by Th62, INCPROJ:def 9;
reconsider S = R as Element of real_projective_plane by INCPROJ:3;
( S in LI1 & S in LI2 ) by A1, A2, INCPROJ:5;
hence L1 meets L2 by XBOOLE_0:def 4; :: thesis: verum