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