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