let AS be AffinSpace; :: thesis: 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; :: thesis: ( x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u implies LIN z,t,u )
assume A1:
( x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u )
; :: thesis: LIN z,t,u
A2:
now assume
x = z
;
:: thesis: LIN z,t,uthen
(
z <> y &
z,
y // z,
t &
z,
y // z,
u )
by A1, Def1;
then
z,
t // z,
u
by Th14;
hence
LIN z,
t,
u
by Def1;
:: thesis: verum end;
now assume A3:
x <> z
;
:: thesis: LIN z,t,u
(
x,
y // x,
z &
x,
y // x,
t &
x,
y // x,
u )
by A1, Def1;
then
(
x,
z // x,
t &
x,
z // x,
u )
by A1, Th14;
then
(
z,
x // z,
t &
z,
x // z,
u )
by DIRAF:47;
then
z,
t // z,
u
by A3, Th14;
hence
LIN z,
t,
u
by Def1;
:: thesis: verum end;
hence
LIN z,t,u
by A2; :: thesis: verum