let v be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A st v in V holds
{[v,d]} is NonatomicND of V,A
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A st v in V holds
{[v,d]} is NonatomicND of V,A
let d be TypeSCNominativeData of V,A; :: thesis: ( v in V implies {[v,d]} is NonatomicND of V,A )
assume v in V ; :: thesis: {[v,d]} is NonatomicND of V,A
then naming (V,A,v,d) = v .--> d by NOMIN_1:def 13
.= {[v,d]} by ZFMISC_1:29 ;
hence {[v,d]} is NonatomicND of V,A ; :: thesis: verum