A1: ND (V,A) c= ND (V,A) ;
defpred S₁[ object ] means gcd_inv_pred V,A,a,b,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
( ( S₁[d] implies p . d = TRUE ) & ( not S₁[d] implies p . d = FALSE ) ) ) ) from PARTPR_2:sch 1(A1);
take p ; :: thesis: ( dom p = ND (V,A) & ( for d being object st d in dom p holds
( ( gcd_inv_pred V,A,a,b,x0,y0,d implies p . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies p . d = FALSE ) ) ) )
thus ( dom p = ND (V,A) & ( for d being object st d in dom p holds
( ( gcd_inv_pred V,A,a,b,x0,y0,d implies p . d = TRUE ) & ( not gcd_inv_pred V,A,a,b,x0,y0,d implies p . d = FALSE ) ) ) ) by A2; :: thesis: verum