:: deftheorem defines are_coplanar PROJDES1:def 1 :
for FCPS being up-3-dimensional CollProjectiveSpace
for a, b, c, d being Element of FCPS holds
( a,b,c,d are_coplanar iff ex x being Element of FCPS st
( a,b,x are_collinear & c,d,x are_collinear ) );