let AS be AffinSpace; for x, y, z, t, u being Element of AS st x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u holds
LIN z,t,u
let x, y, z, t, u be Element of AS; ( x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u implies LIN z,t,u )
assume that
A1:
x <> y
and
A2:
LIN x,y,z
and
A3:
LIN x,y,t
and
A4:
LIN x,y,u
; LIN z,t,u
A5:
now A6:
x,
y // x,
z
by A2, Def1;
x,
y // x,
u
by A4, Def1;
then
x,
z // x,
u
by A1, A6, Th14;
then A7:
z,
x // z,
u
by DIRAF:40;
x,
y // x,
t
by A3, Def1;
then
x,
z // x,
t
by A1, A6, Th14;
then A8:
z,
x // z,
t
by DIRAF:40;
assume
x <> z
;
LIN z,t,uthen
z,
t // z,
u
by A8, A7, Th14;
hence
LIN z,
t,
u
by Def1;
verum end;
now assume A9:
x = z
;
LIN z,t,uthen A10:
z,
y // z,
u
by A4, Def1;
z,
y // z,
t
by A3, A9, Def1;
then
z,
t // z,
u
by A1, A9, A10, Th14;
hence
LIN z,
t,
u
by Def1;
verum end;
hence
LIN z,t,u
by A5; verum