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

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

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

hence
a,a // b,b
by Def1; :: thesis: verumconsider 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;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