let S be OAffinSpace; 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; ( Mid a,b,c implies a,b,c are_collinear )
assume
Mid a,b,c
; 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
; verum