let x be object ; :: thesis: <*x*> is NonatomicND of {1},{x}
take <*(NDSS ({1},{x}))*> ; :: according to NOMIN_1:def 5 :: thesis: ( <*(NDSS ({1},{x}))*> IsNDRankSeq {1},{x} & <*x*> in Union <*(NDSS ({1},{x}))*> )
thus <*(NDSS ({1},{x}))*> IsNDRankSeq {1},{x} by Th27; :: thesis: <*x*> in Union <*(NDSS ({1},{x}))*>
<*x*> in NDSS ({1},{x})

proof

( 1 in {1} & x in {x} ) by TARSKI:def 1;
then <*x*> is Relation of {1},{x} by RELSET_1:3;
hence <*x*> in NDSS ({1},{x}) ; :: thesis: verum

end;

hence <*x*> in Union <*(NDSS ({1},{x}))*> by FINSEQ_3:135; :: thesis: verum