let SAS be Semi_Affine_Space; :: thesis: for o, a, b, a', b' being Element of SAS st o <> a & o <> b & o,a,b is_collinear & o,a,a' is_collinear & o,b,b' is_collinear holds
a,b // a',b'
let o, a, b, a', b' be Element of SAS; :: thesis: ( o <> a & o <> b & o,a,b is_collinear & o,a,a' is_collinear & o,b,b' is_collinear implies a,b // a',b' )
assume A1: ( o <> a & o <> b & o,a,b is_collinear & o,a,a' is_collinear & o,b,b' is_collinear ) ; :: thesis: a,b // a',b'

A2: now

assume o = a' ; :: thesis: a,b // a',b'
then ( a' <> b & a',a // a',b & a',b // a',b' ) by A1, Def2;
then ( a' <> b & a,b // a',b & a',b // a',b' ) by Th18;
hence a,b // a',b' by Th20; :: thesis: verum

end;

now

assume o <> a' ; :: thesis: a,b // a',b'
then ( o <> a' & o <> b & o <> a & o,a // o,b & o,a // o,a' & o,b // o,b' ) by A1, Def2;
then ( o <> a' & o <> b & o,b // a,b & o,b // o,a' & o,b // o,b' ) by Def1, Th18;
then ( o <> a' & o <> b & o,b // a,b & o,b // o,a' & o,a' // o,b' ) by Def1;
then ( o <> a' & a,b // o,a' & o,a' // a',b' ) by Def1, Th18;
hence a,b // a',b' by Th20; :: thesis: verum

end;

hence a,b // a',b' by A2; :: thesis: verum