let X be set ; :: thesis: for S being non empty Subset-Family of X
for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for r being set
for n being Nat holds
( r in F . n iff ex k being Nat st
( k <= n & r in N . k ) )

let S be non empty Subset-Family of X; :: thesis: for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for r being set
for n being Nat holds
( r in F . n iff ex k being Nat st
( k <= n & r in N . k ) )

let N, F be sequence of S; :: thesis: ( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for r being set
for n being Nat holds
( r in F . n iff ex k being Nat st
( k <= n & r in N . k ) ) )

assume that
A1: F . 0 = N . 0 and
A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; :: thesis: for r being set
for n being Nat holds
( r in F . n iff ex k being Nat st
( k <= n & r in N . k ) )

let r be set ; :: thesis: for n being Nat holds
( r in F . n iff ex k being Nat st
( k <= n & r in N . k ) )

let n be Nat; :: thesis: ( r in F . n iff ex k being Nat st
( k <= n & r in N . k ) )

defpred S1[ Nat] means ( ex k being Nat st
( k <= \$1 & r in N . k ) implies r in F . \$1 );
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: ( ex k being Nat st
( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: S1[n + 1]
A5: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2;
given k being Nat such that A6: k <= n + 1 and
A7: r in N . k ; :: thesis: r in F . (n + 1)
( k <= n or k = n + 1 ) by ;
hence r in F . (n + 1) by ; :: thesis: verum
end;
thus ( r in F . n implies ex k being Nat st
( k <= n & r in N . k ) ) :: thesis: ( ex k being Nat st
( k <= n & r in N . k ) implies r in F . n )
proof
defpred S2[ Nat] means r in F . \$1;
assume A8: r in F . n ; :: thesis: ex k being Nat st
( k <= n & r in N . k )

then A9: ex n being Nat st S2[n] ;
ex s being Nat st
( S2[s] & ( for k being Nat st S2[k] holds
s <= k ) ) from then consider s being Nat such that
A10: r in F . s and
A11: for k being Nat st r in F . k holds
s <= k ;
A12: ( ex k being Nat st s = k + 1 implies ex k being Element of NAT st
( k <= n & r in N . k ) )
proof
given k being Nat such that A13: s = k + 1 ; :: thesis: ex k being Element of NAT st
( k <= n & r in N . k )

reconsider k = k as Element of NAT by ORDINAL1:def 12;
A14: not r in F . k
proof
assume r in F . k ; :: thesis: contradiction
then s <= k by A11;
hence contradiction by A13, NAT_1:13; :: thesis: verum
end;
take s ; :: thesis: ( s is Element of NAT & s <= n & r in N . s )
A15: s in NAT by ORDINAL1:def 12;
F . s = (N . s) \/ (F . k) by ;
hence ( s is Element of NAT & s <= n & r in N . s ) by ; :: thesis: verum
end;
( s = 0 implies ex k being Element of NAT st
( k <= n & r in N . k ) ) by ;
hence ex k being Nat st
( k <= n & r in N . k ) by ; :: thesis: verum
end;
A16: S1[ 0 ] by ;
for n being Nat holds S1[n] from NAT_1:sch 2(A16, A3);
hence ( ex k being Nat st
( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: verum