let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, p, q, r being Element of FCPS st p <> q & p,q,r are_collinear & a,b,p,q are_coplanar holds
a,b,p,r are_coplanar
let a, b, p, q, r be Element of FCPS; :: thesis: ( p <> q & p,q,r are_collinear & a,b,p,q are_coplanar implies a,b,p,r are_coplanar )
assume that
A1: ( p <> q & p,q,r are_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 are_collinear and
A4: p,q,x are_collinear by A2;
p,r,x are_collinear by A1, A4, COLLSP:6;
hence a,b,p,r are_coplanar by A3; :: thesis: verum