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