theorem Th8: :: AMI_4:8

for p being set holds
( p in dom Euclid-Function iff ex x, y being Integer st
( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) )