for a, b being pair object st a `1 = b `1 & a `2 = b `2 holds
a = b