defpred S₁[ Nat] means ( D > 0 implies ex o being DoubleReorganization of D st o is D -element );
A1: S₁[ 0 ] ;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
assume i + 1 > 0 ; :: thesis: ex o being DoubleReorganization of D st o is i + 1 -element

per cases ( i = 0 or i > 0 ) ;

suppose A4: i = 0 ; :: thesis: ex o being DoubleReorganization of D st o is i + 1 -element

set F = canFS D;
<*(canFS D)*> is DoubleReorganization of D by Th35;
hence ex o being DoubleReorganization of D st o is i + 1 -element by A4; :: thesis: verum

end;

suppose i > 0 ; :: thesis: ex o being DoubleReorganization of D st o is i + 1 -element

then consider o being DoubleReorganization of D such that
A5: o is i -element by A3;
reconsider e = <*{}*> as DoubleReorganization of {} by Th34;
D misses {} ;
then o ^ e is DoubleReorganization of D \/ {} by Th36;
hence ex o being DoubleReorganization of D st o is i + 1 -element by A5; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence ex b₁ being DoubleReorganization of D st b₁ is n -element ; :: thesis: verum