let SAS be Semi_Affine_Space; :: thesis: for o, a, b, a9, b9 being Element of SAS st o <> a & o <> b & o,a,b is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear holds
a,b // a9,b9
let o, a, b, a9, b9 be Element of SAS; :: thesis: ( o <> a & o <> b & o,a,b is_collinear & o,a,a9 is_collinear & o,b,b9 is_collinear implies a,b // a9,b9 )
assume that
A1: o <> a and
A2: o <> b and
A3: o,a,b is_collinear and
A4: o,a,a9 is_collinear and
A5: o,b,b9 is_collinear ; :: thesis: a,b // a9,b9

A6: now

A7: o,a // o,b by A3, Def2;
o,a // o,a9 by A4, Def2;
then A8: o,b // o,a9 by A1, A7, Def1;
o,b // o,b9 by A5, Def2;
then o,a9 // o,b9 by A2, A8, Def1;
then A9: o,a9 // a9,b9 by Th18;
o,b // a,b by A7, Th18;
then A10: a,b // o,a9 by A2, A8, Def1;
assume o <> a9 ; :: thesis: a,b // a9,b9
hence a,b // a9,b9 by A10, A9, Th20; :: thesis: verum

end;

now

assume A11: o = a9 ; :: thesis: a,b // a9,b9
then a9,a // a9,b by A3, Def2;
then A12: a,b // a9,b by Th18;
a9,b // a9,b9 by A5, A11, Def2;
hence a,b // a9,b9 by A2, A11, A12, Th20; :: thesis: verum

end;

hence a,b // a9,b9 by A6; :: thesis: verum