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 that
A1: ( p <> q & p,q,r is_collinear ) and
A2: a,b,p,q are_coplanar ; :: thesis: a,b,p,r are_coplanar
consider x being Element of FCPS such that
A3: a,b,x is_collinear and
A4: p,q,x is_collinear by A2, Def1;
p,r,x is_collinear by A1, A4, COLLSP:11;
hence a,b,p,r are_coplanar by A3, Def1; :: thesis: verum