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

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