thus ( p <> 0_ (n,L) implies ex d being Nat st
( ex s being bag of n st
( s in Support p & d = degree s ) & ( for s1 being bag of n st s1 in Support p holds
d >= degree s1 ) ) ) :: thesis: ( not p <> 0_ (n,L) implies ex b1 being Nat st b1 = 0 )
proof
assume p <> 0_ (n,L) ; :: thesis: ex d being Nat st
( ex s being bag of n st
( s in Support p & d = degree s ) & ( for s1 being bag of n st s1 in Support p holds
d >= degree s1 ) )

then p <> (dom p) --> (0. L) ;
then consider b being object such that
A1: ( b in dom p & p . b <> 0. L ) by FUNCOP_1:11;
reconsider b = b as bag of n by A1;
defpred S1[ object , object ] means for s being bag of n st s = \$1 holds
\$2 = degree s;
A2: for e being object st e in Support p holds
ex u being object st S1[e,u]
proof
let e be object ; :: thesis: ( e in Support p implies ex u being object st S1[e,u] )
assume e in Support p ; :: thesis: ex u being object st S1[e,u]
then reconsider e = e as bag of n ;
take degree e ; :: thesis: S1[e, degree e]
thus S1[e, degree e] ; :: thesis: verum
end;
consider D being Function such that
A3: ( dom D = Support p & ( for e being object st e in Support p holds
S1[e,D . e] ) ) from b in Support p by ;
then dom D <> {} by ;
then A4: rng D <> {} by RELAT_1:42;
now :: thesis: for y being object st y in rng D holds
y is natural
let y be object ; :: thesis: ( y in rng D implies y is natural )
assume y in rng D ; :: thesis: y is natural
then consider x being object such that
A5: ( x in dom D & y = D . x ) by FUNCT_1:def 3;
reconsider x = x as bag of n by A5, A3;
y = degree x by A5, A3;
hence y is natural ; :: thesis: verum
end;
then reconsider R = rng D as non empty finite natural-membered set by ;
max R in R by XXREAL_2:def 8;
then consider s being object such that
A6: ( s in dom D & max R = D . s ) by FUNCT_1:def 3;
reconsider s = s as bag of n by A6, A3;
reconsider m = max R as Nat by A6;
take m ; :: thesis: ( ex s being bag of n st
( s in Support p & m = degree s ) & ( for s1 being bag of n st s1 in Support p holds
m >= degree s1 ) )

( s in Support p & m = degree s ) by A6, A3;
hence ex s being bag of n st
( s in Support p & m = degree s ) ; :: thesis: for s1 being bag of n st s1 in Support p holds
m >= degree s1

let s1 be bag of n; :: thesis: ( s1 in Support p implies m >= degree s1 )
assume s1 in Support p ; :: thesis: m >= degree s1
then ( D . s1 in R & D . s1 = degree s1 ) by ;
hence m >= degree s1 by XXREAL_2:def 8; :: thesis: verum
end;
thus ( not p <> 0_ (n,L) implies ex b1 being Nat st b1 = 0 ) ; :: thesis: verum