let AFV be WeakAffSegm; :: thesis: for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // c,d
let a, b, c, d be Element of AFV; :: thesis: ( a,b // c,d implies b,a // c,d )
assume a,b // c,d ; :: thesis: b,a // c,d
then c,d // a,b by Th2;
then c,d // b,a by Th3;
hence b,a // c,d by Th2; :: thesis: verum