defpred S₁[ Nat] means ( $1 > card (Support p) or ex M being finite Subset of (Bags n) st
( M c= Support p & card M = $1 & ( for b, b9 being bag of n st b in M & b9 in Support p & b <= b9,T holds
b9 in M ) ) );

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
( k + 1 > card (Support p) or ex M being finite Subset of (Bags n) st
( M c= Support p & card M = k + 1 & ( for b, b9 being bag of n st b in M & b9 in Support p & b <= b9,T holds
b9 in M ) ) )

set R = RelStr(# (Bags n),T #);
assume A4: not k + 1 > card (Support p) ; :: thesis:
k <= k + 1 by NAT_1:11;
then consider M1 being finite Subset of (Bags n) such that
A5: M1 c= Support p and
A6: card M1 = k and
A7: for b, b9 being bag of n st b in M1 & b9 in Support p & b <= b9,T holds
b9 in M1 by A3, A4, XXREAL_0:2;
set G = (Support p) \ M1;

now :: thesis:

let u be object ; :: thesis:
assume u in (Support p) \ M1 ; :: thesis:
then u in Support p by XBOOLE_0:def 5;
hence u in Bags n ; :: thesis:

end;

then reconsider G = (Support p) \ M1 as Subset of (Bags n) by TARSKI:def 3;
A8: for u being object st u in M1 holds
u in Support p by A5;

now :: thesis:

assume G = {} ; :: thesis:
then Support p c= M1 by XBOOLE_1:37;
then for u being object st u in Support p holds
u in M1 ;
then card (Support p) = k by A6, A8, TARSKI:2;
hence contradiction by A4, NAT_1:16; :: thesis:

end;

then reconsider G = G as non empty finite Subset of (Bags n) ;
consider x being Element of RelStr(# (Bags n),T #) such that
A9: x in G and
A10: x is_maximal_wrt G, the InternalRel of RelStr(# (Bags n),T #) by BAGORDER:6;
reconsider b = x as bag of n ;
set M = M1 \/ {b};

now :: thesis:

let u be object ; :: thesis:
assume u in {b} ; :: thesis:
then u = b by TARSKI:def 1;
hence u in Bags n ; :: thesis:

end;

then {b} c= Bags n ;
then M1 \/ {b} c= (Bags n) \/ (Bags n) by XBOOLE_1:13;
then reconsider M = M1 \/ {b} as finite Subset of (Bags n) ;

now :: thesis:

let u be object ; :: thesis:
assume A11: u in M ; :: thesis:

now :: thesis:

per cases by A11, XBOOLE_0:def 3;

case u in M1 ; :: thesis:

hence u in Support p by A5; :: thesis:

end;

case u in {b} ; :: thesis:

then u in G by A9, TARSKI:def 1;
hence u in Support p by XBOOLE_0:def 5; :: thesis:

end;

hence u in Support p ; :: thesis:

end;

then A12: M c= Support p ;

A13: now :: thesis:

let b9 be bag of n; :: thesis:
assume A14: b9 in G ; :: thesis:

now :: thesis:

per cases ;

case b9 = b ; :: thesis:

hence b9 <= b,T by TERMORD:6; :: thesis:

end;

case b9 <> b ; :: thesis:

then not [b,b9] in T by A10, A14, WAYBEL_4:def 23;
then not b <= b9,T by TERMORD:def 2;
then b9 < b,T by TERMORD:5;
hence b9 <= b,T by TERMORD:def 3; :: thesis:

end;

hence b9 <= b,T ; :: thesis:

end;

A15: now :: thesis:

let b1, b2 be bag of n; :: thesis:
assume that
A16: b1 in M and
A17: b2 in Support p and
A18: b1 <= b2,T ; :: thesis:

now :: thesis:

per cases by A16, XBOOLE_0:def 3;

case b1 in M1 ; :: thesis:

then b2 in M1 by A7, A17, A18;
hence b2 in M by XBOOLE_0:def 3; :: thesis:

end;

case b1 in {b} ; :: thesis:

then A19: b1 = b by TARSKI:def 1;

per cases ;

suppose b2 = b1 ; :: thesis:

hence b2 in M by A16; :: thesis:

end;

suppose b2 <> b1 ; :: thesis:

then A20: b1 < b2,T by A18, TERMORD:def 3;
not b2 in G by A20, TERMORD:5, A13, A19;
then b2 in M1 by A17, XBOOLE_0:def 5;
hence b2 in M by XBOOLE_0:def 3; :: thesis:

end;

hence b2 in M ; :: thesis:

end;

not b in M1 by A9, XBOOLE_0:def 5;
then card M = k + 1 by A6, CARD_2:41;
hence ex M being finite Subset of (Bags n) st
( M c= Support p & card M = k + 1 & ( for b, b9 being bag of n st b in M & b9 in Support p & b <= b9,T holds
b9 in M ) ) by A12, A15; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

ex M being finite Subset of (Bags n) st
( M c= Support p & card M = 0 & ( for b, b9 being bag of n st b in M & b9 in Support p & b <= b9,T holds
b9 in M ) )

proof

set M = {} (Bags n);
take {} (Bags n) ; :: thesis:
thus ( {} (Bags n) c= Support p & card ({} (Bags n)) = 0 & ( for b, b9 being bag of n st b in {} (Bags n) & b9 in Support p & b <= b9,T holds
b9 in {} (Bags n) ) ) ; :: thesis:

end;

then A21: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A21, A2);
hence ex b₁ being finite Subset of (Bags n) st
( b₁ c= Support p & card b₁ = i & ( for b, b9 being bag of n st b in b₁ & b9 in Support p & b <= b9,T holds
b9 in b₁ ) ) by A1; :: thesis: