let
G1
,
G2
be
_Graph
;
:: thesis:
(
G1
==
G2
&
G1
is
acyclic
implies
G2
is
acyclic
)
assume
that
A1
:
G1
==
G2
and
A2
:
G1
is
acyclic
;
:: thesis:
G2
is
acyclic
reconsider
G19
=
G1
as
acyclic
_Graph
by
A2
;
G2
is
Subgraph
of
G19
by
A1
,
GLIB_000:87
;
hence
G2
is
acyclic
;
:: thesis:
verum