let AFV be WeakAffVect; :: thesis: for a, b, c being Element of AFV st Mid a,b,c holds
Mid c,b,a
let a, b, c be Element of AFV; :: 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 b,a // c,b by Th8;
then c,b // b,a by Th4;
hence Mid c,b,a by Def3; :: thesis: verum