let a1, v, v1 be object ; :: thesis: for V, A being set st {v,v1} c= V & a1 in A holds
ND_ex_2 (v,v1,a1) is TypeSCNominativeData of V,A
let V, A be set ; :: thesis: ( {v,v1} c= V & a1 in A implies ND_ex_2 (v,v1,a1) is TypeSCNominativeData of V,A )
assume ( {v,v1} c= V & a1 in A ) ; :: thesis: ND_ex_2 (v,v1,a1) is TypeSCNominativeData of V,A
then ND_ex_2 (v,v1,a1) is NonatomicND of V,A by Th49;
hence ND_ex_2 (v,v1,a1) is TypeSCNominativeData of V,A by Def6; :: thesis: verum