let S be OAffinSpace; for x, y, t, z being Element of S st Mid x,y,t & Mid x,z,t & not Mid x,y,z holds
Mid x,z,y
let x, y, t, z be Element of S; ( Mid x,y,t & Mid x,z,t & not Mid x,y,z implies Mid x,z,y )
assume that
A1:
Mid x,y,t
and
A2:
Mid x,z,t
; ( Mid x,y,z or Mid x,z,y )
A3:
x,z // z,t
by A2, Def3;
A4:
x,y // y,t
by A1, Def3;
now
x,
z // x,
t
by A3, ANALOAF:def 5;
then A5:
x,
t // x,
z
by Th5;
assume A6:
x <> t
;
( Mid x,y,z or Mid x,z,y )
x,
y // x,
t
by A4, ANALOAF:def 5;
then
x,
y // x,
z
by A6, A5, Th6;
hence
(
Mid x,
y,
z or
Mid x,
z,
y )
by Th11;
verum end;
hence
( Mid x,y,z or Mid x,z,y )
by A1, A2, Th12; verum