let GF be Graph-yielding Function; :: thesis: ( not GF is empty & GF is loopfull implies not GF is loopless )
assume A1: ( not GF is empty & GF is loopfull ) ; :: thesis: not GF is loopless
then consider x being object such that
A2: x in dom GF by XBOOLE_0:def 1;
consider G being _Graph such that
A3: ( GF . x = G & G is loopfull ) by A1, A2;
thus not GF is loopless by A1, A2, A3; :: thesis: verum