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 )

A1: 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;

assume a,b,c is_collinear ; :: thesis: ( Mid a,b,c or Mid b,a,c or Mid a,c,b )
then A2: a,b '||' a,c by Def5;
( not a,b // a,c or Mid a,b,c or Mid a,c,b ) by Th11;
hence ( Mid a,b,c or Mid b,a,c or Mid a,c,b ) by A2, A1, Def4; :: thesis: verum