let AFV be WeakAffSegm; :: thesis: for a, b, b9, b99 being Element of AFV st a,b9 // a,b99 & a,b // a,b99 & not b = b9 & not b = b99 holds
b9 = b99
let a, b, b9, b99 be Element of AFV; :: thesis: ( a,b9 // a,b99 & a,b // a,b99 & not b = b9 & not b = b99 implies b9 = b99 )
assume A1: ( a,b9 // a,b99 & a,b // a,b99 ) ; :: thesis: ( b = b9 or b = b99 or b9 = b99 )
now :: thesis: ( b9 <> b99 & b <> b99 & not b = b9 & not b = b99 implies b9 = b99 )
assume ( b9 <> b99 & b <> b99 ) ; :: thesis: ( b = b9 or b = b99 or b9 = b99 )
then b9,b // b99,b99 by A1, Def1;
hence ( b = b9 or b = b99 or b9 = b99 ) by Th6; :: thesis: verum
end;
hence ( b = b9 or b = b99 or b9 = b99 ) ; :: thesis: verum