A1: (ND (V,A)) \ A c= ND (V,A) ;
consider p being SCPartialNominativePredicate of V,A such that
A2: dom p = (ND (V,A)) \ A and
A3: 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)) \ A & ( for d being NonatomicND of V,A st d in dom p holds
( ( denaming (v,d) in dom p implies p . d = TRUE ) & ( not denaming (v,d) in dom p implies p . d = FALSE ) ) ) )
thus dom p = (ND (V,A)) \ A by A2; :: thesis: for d being NonatomicND of V,A st d in dom p holds
( ( denaming (v,d) in dom p implies p . d = TRUE ) & ( not denaming (v,d) in dom p implies p . d = FALSE ) )
let d be NonatomicND of V,A; :: thesis: ( d in dom p implies ( ( denaming (v,d) in dom p implies p . d = TRUE ) & ( not denaming (v,d) in dom p implies p . d = FALSE ) ) )
assume A4: d in dom p ; :: thesis: ( ( denaming (v,d) in dom p implies p . d = TRUE ) & ( not denaming (v,d) in dom p implies p . d = FALSE ) )
thus ( denaming (v,d) in dom p implies p . d = TRUE ) by A2, A3, A4; :: thesis: ( not denaming (v,d) in dom p implies p . d = FALSE )
assume not denaming (v,d) in dom p ; :: thesis: p . d = FALSE
then not S₁[d] by A2;
hence p . d = FALSE by A3, A4; :: thesis: verum