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 n 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 n 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 n st b in Support p holds
b <= b₁,T ) ) )

reconsider sp = Support p as finite set by POLYNOM1:def 5;
card sp is finite ;
then consider m being Nat such that
A2: card (Support p) = card m by CARD_1:48;
reconsider sp = Support p as finite Subset of (Bags n) by POLYNOM1:def 5;
defpred S₁[ Nat] means for B being finite Subset of (Bags n) st card B = $1 holds
ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) );
A3: 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 A4: 1 <= k ; :: thesis: ( not S₁[k] or S₁[k + 1] )
thus ( S₁[k] implies S₁[k + 1] ) :: thesis: verum

proof

assume A5: 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 b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) )
assume A6: card B = k + 1 ; :: thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
then reconsider B = B as non empty finite Subset of (Bags n) ;
set x = the Element of B;
reconsider x = the Element of B as Element of Bags n ;
reconsider x = x as bag of n ;
set X = B \ {x};

now :: thesis: for u being object st u in {x} holds
u in B

let u be object ; :: 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 ;
then A7: B = {x} \/ B by XBOOLE_1:12
.= {x} \/ (B \ {x}) by XBOOLE_1:39 ;
( x in B \ {x} iff ( x in B & not x in {x} ) ) by XBOOLE_0:def 5;
then A8: (card (B \ {x})) + 1 = k + 1 by A6, A7, CARD_2:41, TARSKI:def 1;
then reconsider X = B \ {x} as non empty set by A4;
consider b9 being bag of n such that
A9: b9 in X and
A10: for b being bag of n st b in X holds
[b,b9] in T by A5, A8;
A11: T is_connected_in field T by RELAT_2:def 14;

now :: thesis: ( ( x = b9 & ex b9, b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) ) or ( x <> b9 & ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) ) )

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

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

A13: now :: thesis: for b being bag of n st b in B holds
[b,b9] in T

let b be bag of n; :: thesis: ( b in B implies [b,b9] in T )
assume A14: b in B ; :: thesis: [b,b9] in T

now :: thesis: ( ( b in X & [b,b9] in T ) or ( not b in X & [b,b9] in T ) )

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

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

hence [b,b9] in T by A10; :: thesis: verum

end;

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

then b in {x} by A7, A14, XBOOLE_0:def 3;
then b = x by TARSKI:def 1;
hence [b,b9] in T by A12, ORDERS_1:3; :: thesis: verum

end;

end;

end;

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

end;

take b9 = b9; :: thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
X c= B by XBOOLE_1:36;
hence ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) by A9, A13; :: thesis: verum

end;

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

b9 is Element of Bags n by PRE_POLY:def 12;
then [b9,b9] in T by ORDERS_1:3;
then A16: b9 in field T by RELAT_1:15;
[x,x] in T by ORDERS_1:3;
then A17: x in field T by RELAT_1:15;

now :: thesis: ( ( [x,b9] in T & ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) ) or ( [b9,x] in T & ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) ) )

per cases ( [x,b9] in T or [b9,x] in T ) by A11, A15, A17, A16, RELAT_2:def 6;

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

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

proof

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

proof

let b be bag of n; :: thesis: ( b in B implies [b,b9] in T )
assume A19: b in B ; :: thesis: [b,b9] in T

now :: thesis: ( ( b <> x & [b,b9] in T ) or ( b = x & [b,b9] in T ) )

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

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

then not b in {x} by TARSKI:def 1;
then b in X by A19, XBOOLE_0:def 5;
hence [b,b9] in T by A10; :: thesis: verum

end;

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

hence [b,b9] in T by A18; :: thesis: verum

end;

end;

end;

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

end;

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

end;

end;

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

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

proof

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

proof

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

now :: thesis: ( ( b <> x & [b,x] in T ) or ( b = x & [b,x] in T ) )

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 A21, XBOOLE_0:def 5;
then A22: [b,b9] in T by A10;
( b is Element of Bags n & b9 is Element of Bags n ) by PRE_POLY:def 12;
hence [b,x] in T by A20, A22, ORDERS_1:5; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

end;

end;

end;

end;

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

end;

end;

end;

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

end;

end;

end;

m <> 0 by A1, A2;
then A23: 1 <= m by NAT_1:14;
A24: card (Support p) = m by A2;
A25: S₁[1]

proof

let B be finite Subset of (Bags n); :: thesis: ( card B = 1 implies ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) ) )
assume card B = 1 ; :: thesis: ex b9 being bag of n st
( b9 in B & ( for b being bag of n st b in B holds
[b,b9] in T ) )
then card {{}} = card B by CARD_1:30;
then consider b being object such that
A26: B = {b} by CARD_1:29;
A27: b in B by A26, TARSKI:def 1;
then reconsider b = b as Element of Bags n ;
reconsider b = b as bag of n ;

now :: thesis: for b9 being bag of n st b9 in B holds
[b9,b] in T

let b9 be bag of n; :: thesis: ( b9 in B implies [b9,b] in T )
assume b9 in B ; :: thesis: [b9,b] in T
then b9 = b by A26, TARSKI:def 1;
hence [b9,b] in T by ORDERS_1:3; :: thesis: verum

end;

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

end;

for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A25, A3);
then consider b9 being bag of n such that
A28: b9 in sp and
A29: for b being bag of n st b in sp holds
[b,b9] in T by A24, A23;
take b9 ; :: thesis: ( b9 is Element of Bags n & b9 is Element of Bags n & not ( not ( Support p = {} & b9 = EmptyBag n ) & not ( b9 in Support p & ( for b being bag of n st b in Support p holds
b <= b9,T ) ) ) )
for b being bag of n st b in sp holds
b <= b9,T by A29;
hence ( b9 is Element of Bags n & b9 is Element of Bags n & not ( not ( Support p = {} & b9 = EmptyBag n ) & not ( b9 in Support p & ( for b being bag of n st b in Support p holds
b <= b9,T ) ) ) ) by A28; :: thesis: verum

end;

end;