let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS st a <> b & a,b,c are_collinear & a,b // c,d holds
a,c // b,d
let a, b, c, d be Element of SAS; ( a <> b & a,b,c are_collinear & a,b // c,d implies a,c // b,d )
assume that
A1:
a <> b
and
A2:
a,b,c are_collinear
and
A3:
a,b // c,d
; a,c // b,d
now ( b <> c implies a,c // b,d )A4:
a,
b // a,
c
by A2;
then
a,
b // c,
b
by Th7;
then
c,
b // c,
d
by A1, A3, Def1;
then A5:
b,
c // b,
d
by Th7;
assume A6:
b <> c
;
a,c // b,d
b,
c // a,
c
by A4, Th7;
hence
a,
c // b,
d
by A6, A5, Def1;
verum end;
hence
a,c // b,d
by A3; verum