let S be OAffinSpace; :: thesis: for a, b, c being Element of S st Mid a,b,c holds
a,b,c are_collinear
let a, b, c be Element of S; :: thesis: ( Mid a,b,c implies a,b,c are_collinear )
assume Mid a,b,c ; :: thesis: a,b,c are_collinear
then a,b // b,c ;
then a,b // a,c by ANALOAF:def 5;
then a,b '||' a,c ;
hence a,b,c are_collinear ; :: thesis: verum