bityzba lujvo

x1=b1=z1 ensures x2=z2=b2 is true / the case by doing / with means / with proof x3=z3; x1 makes certain x2.