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, b' being bag of n st b in M & b' in Support p & b <= b',T holds
b' in M ) ) );
A2: S₁[ 0 ]

proof

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

proof

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

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

A3: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: 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, b' being bag of n st b in M & b' in Support p & b <= b',T holds
b' in M ) ) )

proof

assume A5: 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, b' being bag of n st b in M & b' in Support p & b <= b',T holds
b' in M ) )
k <= k + 1 by NAT_1:11;
then consider M1 being finite Subset of (Bags n) such that
A6: ( M1 c= Support p & card M1 = k & ( for b, b' being bag of n st b in M1 & b' in Support p & b <= b',T holds
b' in M1 ) ) by A4, A5, XXREAL_0:2;
A7: for u being set st u in M1 holds
u in Support p by A6;
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;

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, A7, TARSKI:2;
hence contradiction by A5, NAT_1:16; :: thesis: verum

end;

then reconsider G = G as non empty finite Subset of (Bags n) ;
set R = RelStr(# (Bags n),T #);
consider x being Element of RelStr(# (Bags n),T #) such that
A8: ( x in G & x is_maximal_wrt G,the InternalRel of RelStr(# (Bags n),T #) ) by BAGORDER:7;
reconsider b = x as bag of n by POLYNOM1:def 14;

A9: now

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

now

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

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

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

end;

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

then not [b,b'] in T by A8, A10, WAYBEL_4:def 24;
then not b <= b',T by TERMORD:def 2;
then b' < b,T by TERMORD:5;
hence b' <= b,T by TERMORD:def 3; :: thesis: verum

end;

end;

end;

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

end;

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 A6; :: thesis: verum

end;

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

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

now

let b1, b2 be bag of n; :: thesis: ( b1 in M & b2 in Support p & b1 <= b2,T implies b2 in M )
assume A14: ( b1 in M & b2 in Support p & b1 <= b2,T ) ; :: thesis: b2 in M

now

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

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

then b2 in M1 by A6, A14;
hence b2 in M by XBOOLE_0:def 3; :: thesis: verum

end;

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

then A15: ( b1 = b & b1 in G ) by A8, TARSKI:def 1;

now

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

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

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

end;

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

then A16: b1 < b2,T by A14, TERMORD:def 3;

now

assume b2 in G ; :: thesis: contradiction
then b2 <= b1,T by A9, A15;
hence contradiction by A16, TERMORD:5; :: thesis: verum

end;

then b2 in M1 by A14, 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;

hence ex M being finite Subset of (Bags n) st
( M c= Support p & card M = k + 1 & ( for b, b' being bag of n st b in M & b' in Support p & b <= b',T holds
b' in M ) ) by A12, A13; :: thesis: verum

end;

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
hence ex b₁ being finite Subset of (Bags n) st
( b₁ c= Support p & card b₁ = i & ( for b, b' being bag of n st b in b₁ & b' in Support p & b <= b',T holds
b' in b₁ ) ) by A1; :: thesis: verum