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

now

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

end;

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