:: deftheorem defines constitute_a_quadrangle PROJDES1:def 2 :
for FCPS being up-3-dimensional CollProjectiveSpace
for o, a, b, c being Element of FCPS holds
( o,a,b,c constitute_a_quadrangle iff ( not a,b,c are_collinear & not o,a,b are_collinear & not o,b,c are_collinear & not o,c,a are_collinear ) );