let S be OAffinSpace; :: thesis: for x, y, z being Element of S holds
( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) )
let x, y, z be Element of S; :: thesis: ( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) )
( x,y // x,z iff ( x,y // y,z or x,z // z,y ) ) by Th9;
hence ( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) ) by Def3; :: thesis: verum