let AFV be WeakAffVect; 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; ( 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
; 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; verum