let AFV be WeakAffVect; for a, b, c, d, b9 being Element of AFV st a,b // c,d & a,c // b9,d holds
b = b9
let a, b, c, d, b9 be Element of AFV; ( a,b // c,d & a,c // b9,d implies b = b9 )
assume that
A1:
a,b // c,d
and
A2:
a,c // b9,d
; b = b9
a,c // b,d
by A1, Def1;
then
b,d // a,c
by Th3;
then A3:
d,b // c,a
by Th7;
b9,d // a,c
by A2, Th3;
then
d,b9 // c,a
by Th7;
then
d,b // d,b9
by A3, Def1;
hence
b = b9
by Th4; verum