let AFV be WeakAffVect; :: thesis: for a, b, c, d, f, a9, b9, c9, d9, f9 being Element of AFV st a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 holds
a,f // a9,f9
let a, b, c, d, f, a9, b9, c9, d9, f9 be Element of AFV; :: thesis: ( a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 implies a,f // a9,f9 )
assume that
A1: a,b // a9,b9 and
A2: c,d // c9,d9 and
A3: b,f // c,d and
A4: b9,f9 // c9,d9 ; :: thesis: a,f // a9,f9
b9,f9 // c,d by A2, A4, Def1;
then A5: b,f // b9,f9 by A3, Def1;
b,a // b9,a9 by A1, Th7;
hence a,f // a9,f9 by A5, Def1; :: thesis: verum