let S be OAffinSpace; :: thesis: for a, b, c being Element of S st Mid a,b,c holds
Mid c,b,a
let a, b, c be Element of S; :: thesis: ( Mid a,b,c implies Mid c,b,a )
assume Mid a,b,c ; :: thesis: Mid c,b,a
then a,b // b,c by Def3;
then c,b // b,a by Th5;
hence Mid c,b,a by Def3; :: thesis: verum