set D = ((U *) \ {{}}) * ;
let p be Element of ((U *) \ {{}}) * ; :: thesis: ( not p is empty implies not p is empty-yielding )
assume not p is empty ; :: thesis: not p is empty-yielding
then consider m being Nat such that
A1: m + 1 = len p by NAT_1:6;
reconsider pp = p as (U *) \ {{}} -valued 1 + m -element FinSequence by A1, CARD_1:def 7;
{(pp . 1)} \ ((U *) \ {{}}) = {} ;
then pp . 1 in (U *) \ {{}} by ZFMISC_1:60;
then ( p . 1 in U * & not p . 1 in {{}} ) by XBOOLE_0:def 5;
then p . 1 <> {} by TARSKI:def 1;
hence not p is empty-yielding ; :: thesis: verum