:: deftheorem defines qtrap SEMI_AF1:def 9 :
for SAS being Semi_Affine_Space
for o, p being Element of SAS holds
( qtrap o,p iff for b, c being Element of SAS ex d being Element of SAS st
( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) ) );