let AFV be WeakAffSegm; :: thesis: for a, b being Element of AFV holds a,b // a,b

let a, b be Element of AFV; :: thesis: a,b // a,b

a,b // b,a by Def1;

hence a,b // a,b by Def1; :: thesis: verum

let a, b be Element of AFV; :: thesis: a,b // a,b

a,b // b,a by Def1;

hence a,b // a,b by Def1; :: thesis: verum