This one assures that result
is the greatest of all common divisors.
∀t:Integer·t>0 & x mod t=0 & y mod t = 0 ⇒ result mod t = 0
It says that any t
, which is a common divisor of x
and y
, is also a divisor of result
EDIT: you should read the above line like this:
∀t:Integer·((t>0 & x mod t=0 & y mod t = 0) ⇒ result mod t = 0)