( not
x
in
the
carrier
of
N
or not
x
in
the
carrier'
of
N
)
by
Th4
;
hence
ex
b
_{1}
being
set
st
( (
x
in
the
carrier
of
N
implies
b
_{1}
=
{
x
}
) & (
x
in
the
carrier'
of
N
implies
b
_{1}
=
Pre
(
N
,
x
) ) ) ;
:: thesis:
verum