let x be object ; :: thesis: for V, A being set st x in NDSS (V,A) holds
x is TypeSSNominativeData of V,A
let V, A be set ; :: thesis: ( x in NDSS (V,A) implies x is TypeSSNominativeData of V,A )
assume x in NDSS (V,A) ; :: thesis: x is TypeSSNominativeData of V,A
then ex w being TypeSSNominativeData of V,A st x = w ;
hence x is TypeSSNominativeData of V,A ; :: thesis: verum