let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: not for a, b, c, d being Element of FCPS holds a,b,c,d are_coplanar
consider a, b, c, d being Element of FCPS such that
A1: for x being Element of FCPS holds
( not a,b,x are_collinear or not c,d,x are_collinear ) by ANPROJ_2:def 14;
take a ; :: thesis: not for b, c, d being Element of FCPS holds a,b,c,d are_coplanar
take b ; :: thesis: not for c, d being Element of FCPS holds a,b,c,d are_coplanar
take c ; :: thesis: not for d being Element of FCPS holds a,b,c,d are_coplanar
take d ; :: thesis: not a,b,c,d are_coplanar
thus not a,b,c,d are_coplanar by A1; :: thesis: verum