let l be Element of ProjectiveLines real_projective_plane; :: thesis: for P, Q, R being Point of real_projective_plane st P in l & Q in l & R in l holds
P,Q,R are_collinear
let P, Q, R be Point of real_projective_plane; :: thesis: ( P in l & Q in l & R in l implies P,Q,R are_collinear )
assume A1: ( P in l & Q in l & R in l ) ; :: thesis: P,Q,R are_collinear
l is LINE of real_projective_plane by INCPROJ:1;
hence P,Q,R are_collinear by A1, COLLSP:16; :: thesis: verum