set O = T;

per cases ( Support p = {} or Support p <> {} ) ;

suppose Support p = {} ; :: thesis: ex b₁ being Element of Bags n st
( ( Support p = {} & b₁ = EmptyBag n ) or ( b₁ in Support p & ( for b being bag of st b in Support p holds
b <= b₁,T ) ) )

hence ex b₁ being Element of Bags n st
( ( Support p = {} & b₁ = EmptyBag n ) or ( b₁ in Support p & ( for b being bag of st b in Support p holds
b <= b₁,T ) ) ) ; :: thesis: verum

end;

suppose A1: Support p <> {} ; :: thesis: ex b₁ being Element of Bags n st
( ( Support p = {} & b₁ = EmptyBag n ) or ( b₁ in Support p & ( for b being bag of st b in Support p holds
b <= b₁,T ) ) )

defpred S₁[ Nat] means for B being finite Subset of (Bags n) st card B = $1 holds
ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) );
A2: S₁[1]

proof

let B be finite Subset of (Bags n); :: thesis: ( card B = 1 implies ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) )
assume A3: card B = 1 ; :: thesis: ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) )
card {{} } = card B by A3, CARD_1:50;
then consider b being set such that
A4: B = {b} by CARD_1:49;
A5: b in B by A4, TARSKI:def 1;
then reconsider b = b as Element of Bags n ;
reconsider b = b as bag of ;

now

let b' be bag of ; :: thesis: ( b' in B implies [b',b] in T )
assume b' in B ; :: thesis: [b',b] in T
then b' = b by A4, TARSKI:def 1;
hence [b',b] in T by ORDERS_1:12; :: thesis: verum

end;

hence ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) by A5; :: thesis: verum

end;

A6: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume A7: 1 <= k ; :: thesis: ( not S₁[k] or S₁[k + 1] )
thus ( S₁[k] implies S₁[k + 1] ) :: thesis: verum

proof

assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let B be finite Subset of (Bags n); :: thesis: ( card B = k + 1 implies ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) )
assume A9: card B = k + 1 ; :: thesis: ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) )
then reconsider B = B as non empty finite Subset of (Bags n) ;
consider x being Element of B;
( x in B & B c= Bags n ) ;
then reconsider x = x as Element of Bags n ;
reconsider x = x as bag of ;
set X = B \ {x};
A10: ( x in B \ {x} iff ( x in B & not x in {x} ) ) by XBOOLE_0:def 5;

now

let u be set ; :: thesis: ( u in {x} implies u in B )
assume u in {x} ; :: thesis: u in B
then u = x by TARSKI:def 1;
hence u in B ; :: thesis: verum

end;

then {x} c= B by TARSKI:def 3;
then A11: B = {x} \/ B by XBOOLE_1:12
.= {x} \/ (B \ {x}) by XBOOLE_1:39 ;
then A12: (card (B \ {x})) + 1 = k + 1 by A9, A10, CARD_2:54, TARSKI:def 1;
then reconsider X = B \ {x} as non empty set by A7;
consider b' being bag of such that
A13: ( b' in X & ( for b being bag of st b in X holds
[b,b'] in T ) ) by A8, A12;
A14: T is_connected_in field T by RELAT_2:def 14;

now

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

case A15: x = b' ; :: thesis: ex b', b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) )

take b' = b'; :: thesis: ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) )
A16: X c= B by XBOOLE_1:36;

now

let b be bag of ; :: thesis: ( b in B implies [b,b'] in T )
assume A17: b in B ; :: thesis: [b,b'] in T

now

per cases ( b in X or not b in X ) ;

case b in X ; :: thesis: [b,b'] in T

hence [b,b'] in T by A13; :: thesis: verum

end;

case not b in X ; :: thesis: [b,b'] in T

then b in {x} by A11, A17, XBOOLE_0:def 3;
then b = x by TARSKI:def 1;
hence [b,b'] in T by A15, ORDERS_1:12; :: thesis: verum

end;

end;

end;

hence [b,b'] in T ; :: thesis: verum

end;

hence ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) by A13, A16; :: thesis: verum

end;

case A18: x <> b' ; :: thesis: ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) )

A19: [x,x] in T by ORDERS_1:12;
b' is Element of Bags n by POLYNOM1:def 14;
then [b',b'] in T by ORDERS_1:12;
then A20: ( x in field T & b' in field T ) by A19, RELAT_1:30;

now

per cases ( [x,b'] in T or [b',x] in T ) by A14, A18, A20, RELAT_2:def 6;

case A21: [x,b'] in T ; :: thesis: ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) )

thus ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) :: thesis: verum

proof

take b' ; :: thesis: ( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) )
for b being bag of st b in B holds
[b,b'] in T

proof

let b be bag of ; :: thesis: ( b in B implies [b,b'] in T )
assume A22: b in B ; :: thesis: [b,b'] in T

now

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

case b <> x ; :: thesis: [b,b'] in T

then not b in {x} by TARSKI:def 1;
then b in X by A22, XBOOLE_0:def 5;
hence [b,b'] in T by A13; :: thesis: verum

end;

case b = x ; :: thesis: [b,b'] in T

hence [b,b'] in T by A21; :: thesis: verum

end;

end;

end;

hence [b,b'] in T ; :: thesis: verum

end;

hence ( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) by A13, XBOOLE_0:def 5; :: thesis: verum

end;

end;

case A23: [b',x] in T ; :: thesis: ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) )

thus ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) :: thesis: verum

proof

take x ; :: thesis: ( x in B & ( for b being bag of st b in B holds
[b,x] in T ) )
for b being bag of st b in B holds
[b,x] in T

proof

let b be bag of ; :: thesis: ( b in B implies [b,x] in T )
assume A24: b in B ; :: thesis: [b,x] in T

now

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

case b <> x ; :: thesis: [b,x] in T

then not b in {x} by TARSKI:def 1;
then b in X by A24, XBOOLE_0:def 5;
then A25: [b,b'] in T by A13;
( b is Element of Bags n & b' is Element of Bags n ) by POLYNOM1:def 14;
hence [b,x] in T by A23, A25, ORDERS_1:14; :: thesis: verum

end;

case b = x ; :: thesis: [b,x] in T

hence [b,x] in T by ORDERS_1:12; :: thesis: verum

end;

end;

end;

hence [b,x] in T ; :: thesis: verum

end;

hence ( x in B & ( for b being bag of st b in B holds
[b,x] in T ) ) ; :: thesis: verum

end;

end;

end;

end;

hence ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) ; :: thesis: verum

end;

end;

end;

hence ex b' being bag of st
( b' in B & ( for b being bag of st b in B holds
[b,b'] in T ) ) ; :: thesis: verum

end;

thus verum ; :: thesis: verum

end;

end;

A26: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A2, A6);
reconsider sp = Support p as finite set by POLYNOM1:def 10;
card sp is finite ;
then consider m being Nat such that
A27: card (Support p) = card m by CARD_1:86;
A28: card (Support p) = m by A27, CARD_1:def 5;
m <> 0 by A27, A1;
then A29: 1 <= m by NAT_1:14;
reconsider sp = Support p as finite Subset of (Bags n) by POLYNOM1:def 10;
consider b' being bag of such that
A30: ( b' in sp & ( for b being bag of st b in sp holds
[b,b'] in T ) ) by A26, A28, A29;
take b' ; :: thesis: ( b' is Element of Bags n & not ( not ( Support p = {} & b' = EmptyBag n ) & not ( b' in Support p & ( for b being bag of st b in Support p holds
b <= b',T ) ) ) )

now

let b be bag of ; :: thesis: ( b in sp implies b <= b',T )
assume b in sp ; :: thesis: b <= b',T
then [b,b'] in T by A30;
hence b <= b',T by Def2; :: thesis: verum

end;

hence ( b' is Element of Bags n & not ( not ( Support p = {} & b' = EmptyBag n ) & not ( b' in Support p & ( for b being bag of st b in Support p holds
b <= b',T ) ) ) ) by A30; :: thesis: verum

end;

end;