let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, d being Element of FCPS st ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) holds
a,b,c,d are_coplanar
let a, b, c, d be Element of FCPS; :: thesis: ( ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) implies a,b,c,d are_coplanar )
assume A1: ( a,b,c is_collinear or b,c,d is_collinear or c,d,a is_collinear or d,a,b is_collinear ) ; :: thesis: a,b,c,d are_coplanar

A2: now

assume A3: a,b,c is_collinear ; :: thesis: a,b,c,d are_coplanar
c,d,c is_collinear by ANPROJ_2:def 7;
hence a,b,c,d are_coplanar by A3, Def1; :: thesis: verum

end;

A4: now

assume b,c,d is_collinear ; :: thesis: a,b,c,d are_coplanar
then A5: c,d,b is_collinear by Th1;
a,b,b is_collinear by ANPROJ_2:def 7;
hence a,b,c,d are_coplanar by A5, Def1; :: thesis: verum

end;

A6: now

assume A7: c,d,a is_collinear ; :: thesis: a,b,c,d are_coplanar
a,b,a is_collinear by ANPROJ_2:def 7;
hence a,b,c,d are_coplanar by A7, Def1; :: thesis: verum

end;

now

assume d,a,b is_collinear ; :: thesis: a,b,c,d are_coplanar
then A8: a,b,d is_collinear by Th1;
c,d,d is_collinear by ANPROJ_2:def 7;
hence a,b,c,d are_coplanar by A8, Def1; :: thesis: verum

end;

hence a,b,c,d are_coplanar by A1, A2, A4, A6; :: thesis: verum