for SAS being Semi_Affine_Space
for a, b, c being Element of SAS st congr a,a,b,c holds
b = c by Th36;