for SAS being Semi_Affine_Space
for a, b, o, p, q being Element of SAS st congr a,o,o,p & congr b,o,o,q holds
congr a,b,q,p by Th71;