A1:
ND (V,A) c= ND (V,A)
;
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_power_input_pred V,A,val,b0,n0,d implies p . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies p . d = FALSE ) ) ) )
thus
( dom p = ND (V,A) & ( for d being object st d in dom p holds
( ( valid_power_input_pred V,A,val,b0,n0,d implies p . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies p . d = FALSE ) ) ) )
by A2; verum