for x, y being Element of BOOLEAN holds
( add_ovfl (<*x*>,<*y*>) = TRUE iff ( x = TRUE & y = TRUE ) )