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 )

A1: now

A2: c,d,c is_collinear by ANPROJ_2:def 7;
assume a,b,c is_collinear ; :: 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 )
hence ( ( 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 ) by A2, Def1; :: thesis: verum

end;

A3: now

A4: a,b,a is_collinear by ANPROJ_2:def 7;
assume c,d,a is_collinear ; :: 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 )
hence ( ( 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 ) by A4, Def1; :: thesis: verum

end;

A5: now

assume d,a,b is_collinear ; :: 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 )
then A6: a,b,d is_collinear by Th1;
c,d,d is_collinear by ANPROJ_2:def 7;
hence ( ( 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 ) by A6, Def1; :: thesis: verum

end;

A7: now

assume b,c,d is_collinear ; :: 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 )
then A8: c,d,b is_collinear by Th1;
a,b,b is_collinear by ANPROJ_2:def 7;
hence ( ( 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 ) by A8, Def1; :: thesis: verum

end;

assume ( 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
hence a,b,c,d are_coplanar by A1, A7, A3, A5; :: thesis: verum