set f = p |-> p;
reconsider f = p |-> p as bag of Seg p ;
f is positive-yielding ;
hence ex b₁ being bag of Seg p st b₁ is positive-yielding ; :: thesis: verum