let X be set ; :: thesis: for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3)
let b1, b2, b3 be real-valued ManySortedSet of X; :: thesis: (b1 + b2) + b3 = b1 + (b2 + b3)

now

let x be set ; :: thesis: ( x in X implies ((b1 + b2) + b3) . x = (b1 + (b2 + b3)) . x )
assume x in X ; :: thesis: ((b1 + b2) + b3) . x = (b1 + (b2 + b3)) . x
thus ((b1 + b2) + b3) . x = ((b1 + b2) . x) + (b3 . x) by Def5
.= ((b1 . x) + (b2 . x)) + (b3 . x) by Def5
.= (b1 . x) + ((b2 . x) + (b3 . x))
.= (b1 . x) + ((b2 + b3) . x) by Def5
.= (b1 + (b2 + b3)) . x by Def5 ; :: thesis: verum

end;

hence (b1 + b2) + b3 = b1 + (b2 + b3) by PBOOLE:3; :: thesis: verum