reconsider
A
=
{}
as
Subset
of
X
by
XBOOLE_1:2
;
A
=
{}
X
;
then
A1
: (
LAp
A
=
{}
&
UAp
A
=
{}
)
by
ROUGHS_1:18
,
ROUGHS_1:19
;
[
(
LAp
A
)
,
(
UAp
A
)
]
in
[:
(
bool
the
carrier
of
X
)
,
(
bool
the
carrier
of
X
)
:]
by
ZFMISC_1:87
;
hence
[
{}
,
{}
]
is
RoughSet
of
X
by
Def13
,
A1
;
:: thesis:
verum