let S be OAffinSpace; :: thesis: for a, b, c being Element of S holds
( not a,b,c is_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 is_collinear or Mid a,b,c or Mid b,a,c or Mid a,c,b )
assume a,b,c is_collinear ; :: thesis: ( Mid a,b,c or Mid b,a,c or Mid a,c,b )
then A1: a,b '||' a,c by Def5;
A2: ( not a,b // a,c or Mid a,b,c or Mid a,c,b ) by Th11;

now

assume a,b // c,a ; :: thesis: Mid b,a,c
then b,a // a,c by ANALOAF:def 5;
hence Mid b,a,c by Def3; :: thesis: verum

end;

hence ( Mid a,b,c or Mid b,a,c or Mid a,c,b ) by A1, A2, Def4; :: thesis: verum