let V be set ; :: thesis: for A, B being set st A c= B holds
NDSS (V,A) c= NDSS (V,B)
let A, B be set ; :: thesis: ( A c= B implies NDSS (V,A) c= NDSS (V,B) )
assume A1: A c= B ; :: thesis: NDSS (V,A) c= NDSS (V,B)
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in NDSS (V,A) or d in NDSS (V,B) )
assume d in NDSS (V,A) ; :: thesis: d in NDSS (V,B)
then ex w being TypeSSNominativeData of V,A st w = d ;
then d is TypeSSNominativeData of V,B by A1, RELSET_1:7;
hence d in NDSS (V,B) ; :: thesis: verum