let P be Element of BK_model ; :: thesis: for L being LINE of (IncProjSp_of real_projective_plane) ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L )
let L be LINE of (IncProjSp_of real_projective_plane); :: thesis: ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L )
consider p, q being Point of real_projective_plane such that
A2: p <> q and
A3: L = Line (p,q) by BKMODEL1:73;
( P <> p or P <> q ) by A2;
hence ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L ) by A3, COLLSP:10; :: thesis: verum