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