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

now :: thesis: ( a <> b implies a,a // b,b )

consider c being Element of AFV such that
A1: a,c // c,b by Def1;
assume A2: a <> b ; :: thesis: a,a // b,b
c,a // c,b by A1, Th4;
hence a,a // b,b by A2, Def1; :: thesis: verum

end;

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