theorem Th7: :: COUNTERS:39

for x, y being object holds
( dom <%x,y%> = {0,1} & rng <%x,y%> = {x,y} )