:: deftheorem defines valid_gcd_input_pred NOMIN_4:def 23 :
for V, A being set
for x, y being object
for x0, y0 being Nat
for d being object holds
( valid_gcd_input_pred V,A,x,y,x0,y0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & x in dom d1 & y in dom d1 & d1 . x = x0 & d1 . y = y0 ) );