let S be OAffinSpace; :: thesis: for b, c, a, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds
Mid a,c,d
let b, c, a, d be Element of S; :: thesis: ( b <> c & Mid a,b,c & Mid b,c,d implies Mid a,c,d )
assume that
A1: b <> c and
A2: Mid a,b,c and
A3: Mid b,c,d ; :: thesis: Mid a,c,d

now

assume A4: a <> b ; :: thesis: Mid a,c,d
A5: ( a,b // b,c & b,c // c,d ) by A2, A3, Def3;
then A6: a,b // c,d by A1, Th6;
a,b // a,c by A5, ANALOAF:def 5;
then a,c // c,d by A4, A6, ANALOAF:def 5;
hence Mid a,c,d by Def3; :: thesis: verum

end;

hence Mid a,c,d by A3; :: thesis: verum