:: deftheorem defines is_a_quadrangle PROJPL_1:def 6 :
for G being IncProjStr
for a, b, c, d being POINT of G holds
( a,b,c,d is_a_quadrangle iff ( a,b,c is_a_triangle & b,c,d is_a_triangle & c,d,a is_a_triangle & d,a,b is_a_triangle ) );