let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, d being Element of st a,b,c,d are_coplanar holds
b,a,c,d are_coplanar
let a, b, c, d be Element of ; :: thesis: ( a,b,c,d are_coplanar implies b,a,c,d are_coplanar )
assume a,b,c,d are_coplanar ; :: thesis: b,a,c,d are_coplanar
then consider x being Element of such that
A1: a,b,x is_collinear and
A2: c,d,x is_collinear by Def1;
b,a,x is_collinear by A1, Th1;
hence b,a,c,d are_coplanar by A2, Def1; :: thesis: verum