let S be OAffinSpace; :: thesis: for x, y being Element of S holds
( Mid x,x,y & Mid x,y,y )
let x, y be Element of S; :: thesis: ( Mid x,x,y & Mid x,y,y )
( x,x // x,y & x,y // y,y ) by Th7;
hence ( Mid x,x,y & Mid x,y,y ) by Def3; :: thesis: verum