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