let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for p, q, r, a, b being Element of FCPS st p <> q & p,q,r is_collinear & a,b,p,q are_coplanar holds
a,b,p,r are_coplanar
let p, q, r, a, b be Element of FCPS; :: thesis: ( p <> q & p,q,r is_collinear & a,b,p,q are_coplanar implies a,b,p,r are_coplanar )
assume A1: ( p <> q & p,q,r is_collinear & a,b,p,q are_coplanar ) ; :: thesis: a,b,p,r are_coplanar
then consider x being Element of FCPS such that
A2: ( a,b,x is_collinear & p,q,x is_collinear ) by Def1;
( a,b,x is_collinear & p,r,x is_collinear ) by A1, A2, COLLSP:11;
hence a,b,p,r are_coplanar by Def1; :: thesis: verum