for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS st trap a,b,c,d,b holds
b = d by Th93, Th94;