defpred S1[ Nat] means ( \$1 > card () 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 ) ) );
A2: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
( k + 1 > card () 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 ) ) )
proof
set R = RelStr(# (Bags n),T #);
assume A4: not k + 1 > card () ; :: thesis: 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 ) )

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 ;
set G = () \ M1;
now :: thesis: for u being object st u in () \ M1 holds
u in Bags n
let u be object ; :: thesis: ( u in () \ M1 implies u in Bags n )
assume u in () \ M1 ; :: thesis: u in Bags n
then u in Support p by XBOOLE_0:def 5;
hence u in Bags n ; :: thesis: verum
end;
then reconsider G = () \ 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;
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: for u being object st u in {b} holds
u in Bags n
let u be object ; :: thesis: ( u in {b} implies u in Bags n )
assume u in {b} ; :: thesis: u in Bags n
then u = b by TARSKI:def 1;
hence u in Bags n ; :: thesis: verum
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: for u being object st u in M holds
u in Support p
let u be object ; :: thesis: ( u in M implies u in Support p )
assume A11: u in M ; :: thesis:
now :: thesis: ( ( u in M1 & u in Support p ) or ( u in {b} & u in Support p ) )end;
hence u in Support p ; :: thesis: verum
end;
then A12: M c= Support p ;
A13: now :: thesis: for b9 being bag of n st b9 in G holds
b9 <= b,T
let b9 be bag of n; :: thesis: ( b9 in G implies b9 <= b,T )
assume A14: b9 in G ; :: thesis: b9 <= b,T
now :: thesis: ( ( b9 = b & b9 <= b,T ) or ( b9 <> b & b9 <= b,T ) )end;
hence b9 <= b,T ; :: thesis: verum
end;
A15: now :: thesis: for b1, b2 being bag of n st b1 in M & b2 in Support p & b1 <= b2,T holds
b2 in M
let b1, b2 be bag of n; :: thesis: ( b1 in M & b2 in Support p & b1 <= b2,T implies b2 in M )
assume that
A16: b1 in M and
A17: b2 in Support p and
A18: b1 <= b2,T ; :: thesis: b2 in M
now :: thesis: ( ( b1 in M1 & b2 in M ) or ( b1 in {b} & b2 in M ) )end;
hence b2 in M ; :: thesis: verum
end;
not b in M1 by ;
then card M = k + 1 by ;
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 ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
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: ( {} (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) ) )

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: verum
end;
then A21: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A21, A2);
hence ex b1 being finite Subset of (Bags n) st
( b1 c= Support p & card b1 = i & ( for b, b9 being bag of n st b in b1 & b9 in Support p & b <= b9,T holds
b9 in b1 ) ) by A1; :: thesis: verum