theorem Th17: :: SEMI_AF1:17
for SAS being Semi_Affine_Space
for a, b, c, p, r being Element of SAS st not a,b // a,c & a,c // p,r & b,c // p,r holds
p = r