hereby :: thesis: ( ( for x being Element of dom GF holds not GF . x is _trivial ) implies GF is non-trivial )

assume A1: GF is non-trivial ; :: thesis: for x being Element of dom GF holds not GF . x is _trivial
let x be Element of dom GF; :: thesis: not GF . x is _trivial
consider G being _Graph such that
A2: ( GF . x = G & not G is _trivial ) by A1;
thus not GF . x is _trivial by A2; :: thesis: verum

end;

assume A3: for x being Element of dom GF holds not GF . x is _trivial ; :: thesis: GF is non-trivial
let x be object ; :: according to GLIB_000:def 61 :: thesis: ( x in dom GF implies ex G being _Graph st
( GF . x = G & not G is _trivial ) )
assume x in dom GF ; :: thesis: ex G being _Graph st
( GF . x = G & not G is _trivial )
then reconsider y = x as Element of dom GF ;
take GF . y ; :: thesis: ( GF . x = GF . y & not GF . y is _trivial )
thus ( GF . x = GF . y & not GF . y is _trivial ) by A3; :: thesis: verum