let S be OAffinSpace; :: thesis: 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; :: thesis: ( Mid x,y,t & Mid x,z,t & not Mid x,y,z implies Mid x,z,y )
assume A1:
( Mid x,y,t & Mid x,z,t )
; :: thesis: ( Mid x,y,z or Mid x,z,y )
then A2:
( x,y // y,t & x,z // z,t )
by Def3;
now assume A3:
x <> t
;
:: thesis: ( Mid x,y,z or Mid x,z,y )
(
x,
y // x,
t &
x,
z // x,
t )
by A2, ANALOAF:def 5;
then
(
x,
y // x,
t &
x,
t // x,
z )
by Th5;
then
x,
y // x,
z
by A3, Th6;
hence
(
Mid x,
y,
z or
Mid x,
z,
y )
by Th11;
:: thesis: verum end;
hence
( Mid x,y,z or Mid x,z,y )
by A1, Th12; :: thesis: verum