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