for SAS being Semi_Affine_Space
for b, c, o, p being Element of SAS st not o,p,c are_collinear & o,p,b are_collinear & qtrap o,p holds
ex d being Element of SAS st trap p,b,c,d,o