let V, A be set ; 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; for d being set st d c= D holds
d is NonatomicND of V,A
let d be set ; ( d c= D implies d is NonatomicND of V,A )
assume A1:
d c= D
; 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 d in Union S
1
<= x
by A4, FINSEQ_3:25;
per cases then
( x = 1 or x > 1 )
by XXREAL_0:1;
suppose A7:
x > 1
;
d in Union Sthen 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;
verum end; end; end;
hence
d is NonatomicND of V,A
by A2, Def5; verum