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 ;
then b,a // c,b by Th7;
then c,b // b,a by Th3;
hence Mid c,b,a ; :: thesis: verum