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

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