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;

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

hence
d is NonatomicND of V,A
by A2, Def5; :: thesis: verum
1 <= x
by A4, FINSEQ_3:25;

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

end;

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;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

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;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