let S be OAffinSpace; :: thesis: for x, y, z, t 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, z, t be Element of S; :: thesis: ( 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 ; :: thesis: ( Mid x,y,z or Mid x,z,y )
A3: x,z // z,t by A2;
A4: x,y // y,t by A1;

now :: thesis: ( x <> t & not Mid x,y,z implies Mid x,z,y )

x,z // x,t by A3, ANALOAF:def 5;
then A5: x,t // x,z by Th2;
assume A6: x <> t ; :: thesis: ( 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, Th3;
hence ( Mid x,y,z or Mid x,z,y ) by Th7; :: thesis: verum

end;

hence ( Mid x,y,z or Mid x,z,y ) by A1, A2, Th8; :: thesis: verum