let AFV be WeakAffSegm; 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; ( a,b // c,d implies b,a // c,d )
assume
a,b // c,d
; 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; verum