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})

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

hence
<*x*> in Union <*(NDSS ({1},{x}))*>
by FINSEQ_3:135; :: thesis: verum
( 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;then <*x*> is Relation of {1},{x} by RELSET_1:3;

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