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 is_collinear & c,d,x is_collinear ) by Def1;
A2: b,x,a is_collinear by A1, Th1;
x,c,d is_collinear by A1, Th1;
then consider y being Element of FCPS such that
A3: ( b,c,y is_collinear & a,d,y is_collinear ) by A2, ANPROJ_2:def 9;
( b,c,y is_collinear & d,a,y is_collinear ) by A3, Th1;
hence b,c,d,a are_coplanar by Def1; :: thesis: verum