let AFV be WeakAffSegm; :: thesis: for a, b, c being Element of AFV st a,b // c,c holds
a = b
let a, b, c be Element of AFV; :: thesis: ( a,b // c,c implies a = b )
assume A1: a,b // c,c ; :: thesis: a = b
a,a // c,c by Th5;
then a,b // a,a by A1, Def1;
hence a = b by Def1; :: thesis: verum