let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, d being Element of FCPS st ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) holds
a,b,c,d are_coplanar
let a, b, c, d be Element of FCPS; :: thesis: ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
A1: now :: thesis: ( a,b,c are_collinear & ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
A2: c,d,c are_collinear by ANPROJ_2:def 7;
assume a,b,c are_collinear ; :: thesis: ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
hence ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar ) by A2; :: thesis: verum
end;
A3: now :: thesis: ( c,d,a are_collinear & ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
A4: a,b,a are_collinear by ANPROJ_2:def 7;
assume c,d,a are_collinear ; :: thesis: ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
hence ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar ) by A4; :: thesis: verum
end;
A5: now :: thesis: ( d,a,b are_collinear & ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
assume d,a,b are_collinear ; :: thesis: ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
then A6: a,b,d are_collinear by Th1;
c,d,d are_collinear by ANPROJ_2:def 7;
hence ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar ) by A6; :: thesis: verum
end;
A7: now :: thesis: ( b,c,d are_collinear & ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
assume b,c,d are_collinear ; :: thesis: ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar )
then A8: c,d,b are_collinear by Th1;
a,b,b are_collinear by ANPROJ_2:def 7;
hence ( ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) implies a,b,c,d are_coplanar ) by A8; :: thesis: verum
end;
assume ( a,b,c are_collinear or b,c,d are_collinear or c,d,a are_collinear or d,a,b are_collinear ) ; :: thesis: a,b,c,d are_coplanar
hence a,b,c,d are_coplanar by A1, A7, A3, A5; :: thesis: verum