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