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

now :: thesis: ( a <> c implies Mid b,c,d )

A3: a,b // b,c by A1;
then a,b // a,c by ANALOAF:def 5;
then A4: ( b,c // a,c or a = b ) by A3, ANALOAF:def 5;
assume A5: a <> c ; :: thesis: Mid b,c,d
a,c // c,d by A2;
then b,c // c,d by A5, A4, Th3;
hence Mid b,c,d ; :: thesis: verum

end;

hence Mid b,c,d by A1, A2, Th8; :: thesis: verum