theorem Th6: :: TOPALG_7:6

for x, y being Point of I[01] holds I[01]-TIMES . (x,y) = x * y