let AFV be WeakAffVect; :: thesis: for a, b, a', b', c, d, c', d', f, f' being Element of 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 ; :: thesis: ( a,b // a',b' & c,d // c',d' & b,f // c,d & b',f' // c',d' implies a,f // a',f' )
assume that
A1: a,b // a',b' and
A2: c,d // c',d' and
A3: b,f // c,d and
A4: b',f' // c',d' ; :: thesis: a,f // a',f'
b',f' // c,d by A2, A4, Def1;
then A5: b,f // b',f' by A3, Def1;
b,a // b',a' by A1, Th8;
hence a,f // a',f' by A5, Def1; :: thesis: verum