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

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