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

A3: a,b // b,c by A1, Def3;
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, Def3;
then b,c // c,d by A5, A4, Th6;
hence Mid b,c,d by Def3; :: thesis: verum

end;

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