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