let a, v be object ; :: thesis: for V, A being set st v in V & a in A holds
ND_ex_1 (v,a) is TypeSCNominativeData of V,A
let V, A be set ; :: thesis: ( v in V & a in A implies ND_ex_1 (v,a) is TypeSCNominativeData of V,A )
assume ( v in V & a in A ) ; :: thesis: ND_ex_1 (v,a) is TypeSCNominativeData of V,A
then ND_ex_1 (v,a) is NonatomicND of V,A by Th46;
hence ND_ex_1 (v,a) is TypeSCNominativeData of V,A by Def6; :: thesis: verum