let x be object ; :: thesis: for V, A being set st x in ND (V,A) holds

x is TypeSCNominativeData of V,A

let V, A be set ; :: thesis: ( x in ND (V,A) implies x is TypeSCNominativeData of V,A )

assume x in ND (V,A) ; :: thesis: x is TypeSCNominativeData of V,A

then ex D being TypeSCNominativeData of V,A st x = D ;

hence x is TypeSCNominativeData of V,A ; :: thesis: verum

x is TypeSCNominativeData of V,A

let V, A be set ; :: thesis: ( x in ND (V,A) implies x is TypeSCNominativeData of V,A )

assume x in ND (V,A) ; :: thesis: x is TypeSCNominativeData of V,A

then ex D being TypeSCNominativeData of V,A st x = D ;

hence x is TypeSCNominativeData of V,A ; :: thesis: verum