let S be OAffinSpace; :: thesis: for a, b, c, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds
Mid a,c,d
let a, b, c, 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 :: thesis: ( a <> b implies Mid a,c,d )

assume A4: a <> b ; :: thesis: Mid a,c,d
A5: a,b // b,c by A2;
b,c // c,d by A3;
then A6: a,b // c,d by A1, A5, Th3;
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 ; :: thesis: verum

end;

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