theorem Th16: :: NOMIN_4:17

for V, A being set
for a, b being Element of V
for x, y being object
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y holds
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_var_init (V,A,a,b,x,y)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))