let AFV be WeakAffSegm; :: thesis: for a, b', b'', b being Element of 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 ; :: thesis: ( a,b' // a,b'' & a,b // a,b'' & not b = b' & not b = b'' implies b' = b'' )
assume A1: ( a,b' // a,b'' & a,b // a,b'' ) ; :: thesis: ( b = b' or b = b'' or b' = b'' )

now

assume ( b' <> b'' & b <> b'' ) ; :: thesis: ( b = b' or b = b'' or b' = b'' )
then b',b // b'',b'' by A1, 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