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