let V, A be set ; :: thesis: for D being NonatomicND of V,A
for d being set st d c= D holds
d is NonatomicND of V,A
let D be NonatomicND of V,A; :: thesis: for d being set st d c= D holds
d is NonatomicND of V,A
let d be set ; :: thesis: ( d c= D implies d is NonatomicND of V,A )
assume A1: d c= D ; :: thesis: d is NonatomicND of V,A
then reconsider d = d as Function ;
consider S being FinSequence such that
A2: S IsNDRankSeq V,A and
A3: D in Union S by Def5;
consider x being object such that
A4: x in dom S and
A5: D in S . x by A3, CARD_5:2;
reconsider x = x as Element of NAT by A4;

now :: thesis: d in Union S

1 <= x by A4, FINSEQ_3:25;

per cases then ( x = 1 or x > 1 ) by XXREAL_0:1;

suppose A6: x = 1 ; :: thesis: d in Union S

then D is TypeSSNominativeData of V,A by A2, A5, Th4;
then d is TypeSSNominativeData of V,A by A1, RELSET_1:1;
then d in NDSS (V,A) ;
hence d in Union S by A2, A4, A6, CARD_5:2; :: thesis: verum

end;

suppose A7: x > 1 ; :: thesis: d in Union S

then reconsider n = x - 1 as Element of NAT by INT_1:5;
A8: S . (n + 1) = NDSS (V,(A \/ (S . n))) by A2, A4, A7, CGAMES_1:20;
then D is TypeSSNominativeData of V,(A \/ (S . n)) by A5, Th4;
then d is TypeSSNominativeData of V,(A \/ (S . n)) by A1, RELSET_1:1;
then d in NDSS (V,(A \/ (S . n))) ;
hence d in Union S by A4, A8, CARD_5:2; :: thesis: verum

end;

end;

end;

hence d is NonatomicND of V,A by A2, Def5; :: thesis: verum