let GF be Graph-yielding Function; :: thesis: ( GF is _trivial & GF is loopless implies GF is edgeless )
assume A1: ( GF is _trivial & GF is loopless ) ; :: thesis: GF is edgeless
let x be object ; :: according to GLIB_008:def 2 :: thesis: ( x in dom GF implies ex G being _Graph st
( GF . x = G & G is edgeless ) )
assume A2: x in dom GF ; :: thesis: ex G being _Graph st
( GF . x = G & G is edgeless )
consider G1 being _Graph such that
A3: ( GF . x = G1 & G1 is _trivial ) by A1, A2, GLIB_000:def 60;
consider G2 being _Graph such that
A4: ( GF . x = G2 & G2 is loopless ) by A1, A2, GLIB_000:def 59;
take G1 ; :: thesis: ( GF . x = G1 & G1 is edgeless )
thus ( GF . x = G1 & G1 is edgeless ) by A3, A4; :: thesis: verum