let X be set ; :: thesis: for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X
for SM being Function of NATPLUS,S
for n being NatPlus
for x being set st x in SM . n holds
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
let S be cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X; :: thesis: for SM being Function of NATPLUS,S
for n being NatPlus
for x being set st x in SM . n holds
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
let SM be Function of NATPLUS,S; :: thesis: for n being NatPlus
for x being set st x in SM . n holds
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
let n be NatPlus; :: thesis: for x being set st x in SM . n holds
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
let x be set ; :: thesis: ( x in SM . n implies ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) ) )
assume A1: x in SM . n ; :: thesis: ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
defpred S₁[ Nat] means ( $1 is NatPlus & ( for y being set st y in SM . $1 holds
ex n1, n0 being NatPlus ex np being Nat st
( $1 = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) ) );
A2: for k being Nat st k >= 1 & ( for l being Nat st l >= 1 & l < k holds
S₁[l] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( k >= 1 & ( for l being Nat st l >= 1 & l < k holds
S₁[l] ) implies S₁[k] )
assume A3: k >= 1 ; :: thesis: ( ex l being Nat st
( l >= 1 & l < k & not S₁[l] ) or S₁[k] )
assume A4: for l being Nat st l >= 1 & l < k holds
S₁[l] ; :: thesis: S₁[k]
A5: k is NatPlus by A3, NAT_LAT:def 6;
for y being set st y in SM . k holds
ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) )

proof

let y be set ; :: thesis: ( y in SM . k implies ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) )
assume A6: y in SM . k ; :: thesis: ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) )
set k0 = k - 1;
reconsider k0 = k - 1 as Nat by A3, CHORD:1;
set n1 = k;
A7: SM . k = ((SM . k) \ (Union (SM | (Seg k0)))) \/ ((SM . k) /\ (Union (SM | (Seg k0)))) by XBOOLE_1:51;
A8: ( y in (SM . k) \ (Union (SM | (Seg k0))) implies ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) )

proof

assume A9: y in (SM . k) \ (Union (SM | (Seg k0))) ; :: thesis: ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) )
k is NatPlus by A3, NAT_LAT:def 6;
hence ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) by A9; :: thesis: verum

end;

( y in (SM . k) /\ (Union (SM | (Seg k0))) implies ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) )

proof

assume y in (SM . k) /\ (Union (SM | (Seg k0))) ; :: thesis: ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) )
then y in Union (SM | (Seg k0)) by XBOOLE_0:def 4;
then consider yy being set such that
A10: ( y in yy & yy in rng (SM | (Seg k0)) ) by TARSKI:def 4;
consider yyy being object such that
A11: ( yyy in dom (SM | (Seg k0)) & yy = (SM | (Seg k0)) . yyy ) by A10, FUNCT_1:def 3;
reconsider yyy = yyy as Nat by A11;
A12: y in SM . yyy by A10, A11, FUNCT_1:47;
A13: ( 1 <= yyy & yyy <= k0 ) by A11, FINSEQ_1:1;
set kk = k - 1;
A14: k - 1 is Nat by A3, CHORD:1;
yyy <= k - 1 by A11, FINSEQ_1:1;
then ( yyy < (k - 1) + 1 & k = (k - 1) + 1 ) by A14, NAT_1:13;
then ( yyy >= 1 & yyy < k ) by A11, FINSEQ_1:1;
then consider n1, n0 being NatPlus, np being Nat such that
A15: ( yyy = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) by A4, A12;
A16: n0 <= k - 1 by A13, A15, XXREAL_0:2;
(k - 1) + 1 = k ;
then A17: k - 1 <= k by INT_1:6;
set n2 = k;
thus ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) by A5, A15, A16, A17, XXREAL_0:2; :: thesis: verum

end;

hence ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) by A6, A7, A8, XBOOLE_0:def 3; :: thesis: verum

end;

hence S₁[k] by A3, NAT_LAT:def 6; :: thesis: verum

end;

A18: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 9(A2);
for k being NatPlus holds S₁[k]

proof

let k be NatPlus; :: thesis: S₁[k]
k >= 1 by CHORD:1;
hence S₁[k] by A18; :: thesis: verum

end;

then consider n1, n0 being NatPlus, np being Nat such that
A19: ( n = n1 & n0 <= n1 & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) ) by A1;
thus ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) ) by A19; :: thesis: verum