let d1, d2 be Nat; :: thesis: ( ( p <> 0_ (n,L) & ex s being bag of n st
( s in Support p & d1 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= d1 ) & ex s being bag of n st
( s in Support p & d2 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= d2 ) implies d1 = d2 ) & ( not p <> 0_ (n,L) & d1 = 0 & d2 = 0 implies d1 = d2 ) )

now :: thesis: ( p <> 0_ (n,L) & ex s being bag of n st
( s in Support p & d1 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
d1 >= degree s1 ) & ex S being bag of n st
( S in Support p & d2 = degree S ) & ( for s1 being bag of n st s1 in Support p holds
d2 >= degree s1 ) implies d1 = d2 )

assume p <> 0_ (n,L) ; :: thesis: ( ex s being bag of n st
( s in Support p & d1 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
d1 >= degree s1 ) & ex S being bag of n st
( S in Support p & d2 = degree S ) & ( for s1 being bag of n st s1 in Support p holds
d2 >= degree s1 ) implies d1 = d2 )
given s being bag of n such that A7: s in Support p and
A8: d1 = degree s ; :: thesis: ( ( for s1 being bag of n st s1 in Support p holds
d1 >= degree s1 ) & ex S being bag of n st
( S in Support p & d2 = degree S ) & ( for s1 being bag of n st s1 in Support p holds
d2 >= degree s1 ) implies d1 = d2 )
assume A9: for s1 being bag of n st s1 in Support p holds
d1 >= degree s1 ; :: thesis: ( ex S being bag of n st
( S in Support p & d2 = degree S ) & ( for s1 being bag of n st s1 in Support p holds
d2 >= degree s1 ) implies d1 = d2 )
given S being bag of n such that A10: S in Support p and
A11: d2 = degree S ; :: thesis: ( ( for s1 being bag of n st s1 in Support p holds
d2 >= degree s1 ) implies d1 = d2 )
assume A12: for s1 being bag of n st s1 in Support p holds
d2 >= degree s1 ; :: thesis: d1 = d2
( d1 <= d2 & d2 <= d1 ) by A7, A8, A9, A10, A11, A12;
hence d1 = d2 by XXREAL_0:1; :: thesis: verum

end;

hence ( ( p <> 0_ (n,L) & ex s being bag of n st
( s in Support p & d1 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= d1 ) & ex s being bag of n st
( s in Support p & d2 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= d2 ) implies d1 = d2 ) & ( not p <> 0_ (n,L) & d1 = 0 & d2 = 0 implies d1 = d2 ) ) ; :: thesis: verum