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

let a, b, c, d be Element of FCPS; :: thesis: ( a,b,c,d are_coplanar implies b,c,d,a are_coplanar )

assume a,b,c,d are_coplanar ; :: thesis: b,c,d,a are_coplanar

then consider x being Element of FCPS such that

A1: ( a,b,x are_collinear & c,d,x are_collinear ) ;

( b,x,a are_collinear & x,c,d are_collinear ) by A1, Th1;

then consider y being Element of FCPS such that

A2: b,c,y are_collinear and

A3: a,d,y are_collinear by ANPROJ_2:def 9;

d,a,y are_collinear by A3, Th1;

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

b,c,d,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 )

assume a,b,c,d are_coplanar ; :: thesis: b,c,d,a are_coplanar

then consider x being Element of FCPS such that

A1: ( a,b,x are_collinear & c,d,x are_collinear ) ;

( b,x,a are_collinear & x,c,d are_collinear ) by A1, Th1;

then consider y being Element of FCPS such that

A2: b,c,y are_collinear and

A3: a,d,y are_collinear by ANPROJ_2:def 9;

d,a,y are_collinear by A3, Th1;

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