let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, d being Element of FCPS st a,b,c,d are_coplanar holds
( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar )
let a, b, c, d be Element of FCPS; :: thesis: ( a,b,c,d are_coplanar implies ( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar ) )
assume A1: a,b,c,d are_coplanar ; :: thesis: ( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar )
then b,a,c,d are_coplanar by Lm2;
then a,c,d,b are_coplanar by Lm3;
then A2: c,d,b,a are_coplanar by Lm3;
then A3: d,b,a,c are_coplanar by Lm3;
then b,d,a,c are_coplanar by Lm2;
then A4: d,a,c,b are_coplanar by Lm3;
then a,c,b,d are_coplanar by Lm3;
then c,a,b,d are_coplanar by Lm2;
then A5: a,b,d,c are_coplanar by Lm3;
then A6: b,d,c,a are_coplanar by Lm3;
then d,c,a,b are_coplanar by Lm3;
then c,d,a,b are_coplanar by Lm2;
then A7: d,a,b,c are_coplanar by Lm3;
then a,d,b,c are_coplanar by Lm2;
then d,b,c,a are_coplanar by Lm3;
then b,c,a,d are_coplanar by Lm3;
hence ( b,c,d,a are_coplanar & c,d,a,b are_coplanar & d,a,b,c are_coplanar & b,a,c,d are_coplanar & c,b,d,a are_coplanar & d,c,a,b are_coplanar & a,d,b,c are_coplanar & a,c,d,b are_coplanar & b,d,a,c are_coplanar & c,a,b,d are_coplanar & d,b,c,a are_coplanar & c,a,d,b are_coplanar & d,b,a,c are_coplanar & a,c,b,d are_coplanar & b,d,c,a are_coplanar & a,b,d,c are_coplanar & a,d,c,b are_coplanar & b,c,a,d are_coplanar & b,a,d,c are_coplanar & c,b,a,d are_coplanar & c,d,b,a are_coplanar & d,a,c,b are_coplanar & d,c,b,a are_coplanar ) by A1, A2, A3, A4, A5, A6, A7, Lm2, Lm3; :: thesis: verum