theorem Th17: :: NOMIN_4:18

for V, A being set
for a, b being Element of V
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))),(SC_assignment ((subtraction (A,a,b)),a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))