defpred S_{1}[ 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 ) ) );

( 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 ) )_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A21, A2);

hence ex b_{1} being finite Subset of (Bags n) st

( b_{1} c= Support p & card b_{1} = i & ( for b, b9 being bag of n st b in b_{1} & b9 in Support p & b <= b9,T holds

b9 in b_{1} ) )
by A1; :: thesis: verum

( 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 S_{1}[k] holds

S_{1}[k + 1]

ex M being finite Subset of (Bags n) st S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[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 ) ) )_{1}[k + 1]
; :: thesis: verum

end;assume A3: S

( 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

hence
S
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;

A8: for u being object st u in M1 holds

u in Support p by A5;

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};

then M1 \/ {b} c= (Bags n) \/ (Bags n) by XBOOLE_1:13;

then reconsider M = M1 \/ {b} as finite Subset of (Bags n) ;

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: verum

end;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 :: thesis: for u being object st u in (Support p) \ M1 holds

u in Bags n

then reconsider G = (Support p) \ M1 as Subset of (Bags n) by TARSKI:def 3;u in Bags n

let u be object ; :: 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;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

A8: for u being object st u in M1 holds

u in Support p by A5;

now :: thesis: not G = {}

then reconsider G = G as non empty finite Subset of (Bags n) ;assume
G = {}
; :: thesis: contradiction

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: verum

end;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: verum

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

then
{b} c= Bags n
;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;assume u in {b} ; :: thesis: u in Bags n

then u = b by TARSKI:def 1;

hence u in Bags n ; :: thesis: verum

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

then A12:
M c= Support p
;u in Support p

let u be object ; :: thesis: ( u in M implies u in Support p )

assume A11: u in M ; :: thesis: u in Support p

hence u in Support p ; :: thesis: verum

end;assume A11: u in M ; :: thesis: u in Support p

hence u in Support p ; :: thesis: verum

A13: now :: thesis: for b9 being bag of n st b9 in G holds

b9 <= b,T

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

end;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: verumper cases
( b9 = b or b9 <> b )
;

end;

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

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: verum

end;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

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

not b in M1
by A9, XBOOLE_0:def 5;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

end;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: verumper cases
( b1 in M1 or b1 in {b} )
by A16, XBOOLE_0:def 3;

end;

case
b1 in {b}
; :: thesis: verum

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

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

end;

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

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: verum

end;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: verum

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: verum

( 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

then A21:
S
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;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

for k being Nat holds S

hence ex b

( b

b9 in b