:: deftheorem Def8 defines Euclidian INT_3:def 8 :
for I being non empty doubleLoopStr holds
( I is Euclidian iff ex f being Function of I,NAT st
for a, b being Element of I st b <> 0. I holds
ex q, r being Element of I st
( a = (q * b) + r & ( r = 0. I or f . r < f . b ) ) );