let AFV be WeakAffSegm; :: thesis: for a, b', b'', b being Element of AFV st a,b' // a,b'' & a,b // a,b'' & not b = b' & not b = b'' holds
b' = b''
let a, b', b'', b be Element of AFV; :: thesis: ( a,b' // a,b'' & a,b // a,b'' & not b = b' & not b = b'' implies b' = b'' )
assume that
A1: a,b' // a,b'' and
A2: a,b // a,b'' ; :: thesis: ( b = b' or b = b'' or b' = b'' )

now

assume that
A3: b' <> b'' and
A4: b <> b'' ; :: thesis: ( b = b' or b = b'' or b' = b'' )
b',b // b'',b'' by A1, A2, A3, A4, Def2;
hence ( b = b' or b = b'' or b' = b'' ) by Th6; :: thesis: verum

end;

hence ( b = b' or b = b'' or b' = b'' ) ; :: thesis: verum