theorem Th56: :: SEMI_AF1:56

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