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 ( x <> z implies LIN z,t,u )A6:
x,
y // x,
z
by A2;
x,
y // x,
u
by A4;
then
x,
z // x,
u
by A1, A6, Th4;
then A7:
z,
x // z,
u
by DIRAF:40;
x,
y // x,
t
by A3;
then
x,
z // x,
t
by A1, A6, Th4;
then A8:
z,
x // z,
t
by DIRAF:40;
assume
x <> z
;
LIN z,t,uthen
z,
t // z,
u
by A8, A7, Th4;
hence
LIN z,
t,
u
;
verum end;
( x = z implies LIN z,t,u )
by A1, A3, A4, Th4;
hence
LIN z,t,u
by A5; verum