A1:
ND (V,A) c= ND (V,A)
;
defpred S1[ object ] means valid_gcd_input_pred V,A,x,y,x0,y0,$1;
consider p being SCPartialNominativePredicate of V,A such that
A2:
( dom p = ND (V,A) & ( for d being object st d in dom p holds
( ( S1[d] implies p . d = TRUE ) & ( not S1[d] implies p . d = FALSE ) ) ) )
from PARTPR_2:sch 1(A1);
take
p
; ( dom p = ND (V,A) & ( for d being object st d in dom p holds
( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies p . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies p . d = FALSE ) ) ) )
thus
( dom p = ND (V,A) & ( for d being object st d in dom p holds
( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies p . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies p . d = FALSE ) ) ) )
by A2; verum