take
N
=
G_Net
(#
{}
,
{}
,
{}
#);
:: thesis:
N
is
GG
( the
escape
of
N
c=
[:
the
carrier
of
N
, the
carrier
of
N
:]
& the
entrance
of
N
*
the
entrance
of
N
=
{}
)
by
XBOOLE_1:2
;
hence
N
is
GG
;
:: thesis:
verum