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