let SAS be 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
let a, a9, b, b9, o be Element of SAS; ( o <> a & o <> b & o,a,b are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear implies a,b // a9,b9 )
assume that
A1:
o <> a
and
A2:
o <> b
and
A3:
o,a,b are_collinear
and
A4:
o,a,a9 are_collinear
and
A5:
o,b,b9 are_collinear
; a,b // a9,b9
A6:
now ( o <> a9 implies a,b // a9,b9 )A7:
o,
a // o,
b
by A3;
o,
a // o,
a9
by A4;
then A8:
o,
b // o,
a9
by A1, A7, Def1;
o,
b // o,
b9
by A5;
then
o,
a9 // o,
b9
by A2, A8, Def1;
then A9:
o,
a9 // a9,
b9
by Th7;
o,
b // a,
b
by A7, Th7;
then A10:
a,
b // o,
a9
by A2, A8, Def1;
assume
o <> a9
;
a,b // a9,b9hence
a,
b // a9,
b9
by A10, A9, Th8;
verum end;
now ( o = a9 implies a,b // a9,b9 )assume A11:
o = a9
;
a,b // a9,b9then
a9,
a // a9,
b
by A3;
then A12:
a,
b // a9,
b
by Th7;
a9,
b // a9,
b9
by A5, A11;
hence
a,
b // a9,
b9
by A2, A11, A12, Th8;
verum end;
hence
a,b // a9,b9
by A6; verum