for SAS being Semi_Affine_Space
for a, a9, b, b9, o being Element of SAS st o <> a & o <> b & o,a,b are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear holds
a,b // a9,b9