defpred S₁[ Element of 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 ) ) );

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
( 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 ) ) )

proof

set R = RelStr(# (Bags n),T #);
assume A4: not k + 1 > card (Support p) ; :: 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 A3, A4, XXREAL_0:2;
set G = (Support p) \ M1;

now

let u be set ; :: thesis: ( u in (Support p) \ M1 implies u in Bags n )
assume u in (Support p) \ 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 = (Support p) \ M1 as Subset of (Bags n) by TARSKI:def 3;
A8: for u being set st u in M1 holds
u in Support p by A5;

now

assume G = {} ; :: thesis: contradiction
then Support p c= M1 by XBOOLE_1:37;
then for u being set 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: verum

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:7;
reconsider b = x as bag of n by PRE_POLY:def 12;
set M = M1 \/ {b};

now

let u be set ; :: 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 by TARSKI:def 3;
then M1 \/ {b} c= (Bags n) \/ (Bags n) by XBOOLE_1:13;
then reconsider M = M1 \/ {b} as finite Subset of (Bags n) ;

now

let u be set ; :: thesis: ( u in M implies u in Support p )
assume A11: u in M ; :: thesis: u in Support p

now

per cases ( u in M1 or u in {b} ) by A11, XBOOLE_0:def 3;

case u in M1 ; :: thesis: u in Support p

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

end;

case u in {b} ; :: thesis: u in Support p

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

end;

end;

end;

hence u in Support p ; :: thesis: verum

end;

then A12: M c= Support p by TARSKI:def 3;

A13: now

let b9 be bag of n; :: thesis: ( b9 in G implies b9 <= b,T )
assume A14: b9 in G ; :: thesis: b9 <= b,T

now

per cases ( b9 = b or b9 <> b ) ;

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

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

end;

case b9 <> b ; :: thesis: b9 <= b,T

then not [b,b9] in T by A10, A14, WAYBEL_4:def 24;
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: verum

end;

end;

end;

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

end;

A15: now

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

per cases ( b1 in M1 or b1 in {b} ) by A16, XBOOLE_0:def 3;

case b1 in M1 ; :: thesis: b2 in M

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

end;

case b1 in {b} ; :: thesis: b2 in M

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

now

per cases ( b2 = b1 or b2 <> b1 ) ;

case b2 = b1 ; :: thesis: b2 in M

hence b2 in M by A16; :: thesis: verum

end;

case b2 <> b1 ; :: thesis: b2 in M

then A20: b1 < b2,T by A18, TERMORD:def 3;

now

assume b2 in G ; :: thesis: contradiction
then b2 <= b1,T by A13, A19;
hence contradiction by A20, TERMORD:5; :: thesis: verum

end;

then b2 in M1 by A17, XBOOLE_0:def 5;
hence b2 in M by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence b2 in M ; :: thesis: verum

end;

end;

end;

hence b2 in M ; :: thesis: verum

end;

not b in M1 by A9, XBOOLE_0:def 5;
then card M = k + 1 by A6, CARD_2:54;
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: verum

end;

hence S₁[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) ) ) by XBOOLE_1:2; :: thesis: verum

end;

then A21: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(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: verum