let AFV be WeakAffVect; :: thesis: for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // d,c
let a, b, c, d be Element of AFV; :: thesis: ( a,b // c,d implies b,a // d,c )
assume A1: a,b // c,d ; :: thesis: b,a // d,c
a,a // c,c by Th6;
hence b,a // d,c by A1, Def1; :: thesis: verum