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