:: deftheorem defines Quadrangle PROJPL_1:def 7 :
for G being IncProjSp
for b₂ being Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] holds
( b₂ is Quadrangle of G iff b₂ `1_4 ,b<sub>2</sub> `2_4 ,b₂ `3_4 ,b<sub>2</sub> `4_4 is_a_quadrangle );