let AS be AffinSpace; for x, y, z, t being Element of AS st x <> y & LIN x,y,z & x,y // z,t holds
LIN x,y,t
let x, y, z, t be Element of AS; ( x <> y & LIN x,y,z & x,y // z,t implies LIN x,y,t )
assume that
A1:
x <> y
and
A2:
LIN x,y,z
and
A3:
x,y // z,t
; LIN x,y,t
now ( z <> x implies LIN x,y,t )
x,
y // x,
z
by A2;
then
x,
z // z,
t
by A1, A3, Th4;
then
z,
x // z,
t
by Th3;
then
LIN z,
x,
t
;
then A4:
LIN x,
z,
t
by Th5;
assume A5:
z <> x
;
LIN x,y,tA6:
LIN x,
z,
x
by Th6;
LIN x,
z,
y
by A2, Th5;
hence
LIN x,
y,
t
by A5, A4, A6, Th7;
verum end;
hence
LIN x,y,t
by A3; verum