:: deftheorem defines gcd_main_part NOMIN_4:def 21 :
for V, A being set
for a, b being Element of V
for x, y being object holds gcd_main_part (V,A,a,b,x,y) = PP_composition ((gcd_var_init (V,A,a,b,x,y)),(gcd_main_loop (V,A,a,b)));