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