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