reconsider
A
=
[#]
X
as
Subset
of
X
;
A1
: (
LAp
A
=
[#]
X
&
UAp
A
=
[#]
X
)
by
ROUGHS_1:20
,
ROUGHS_1:21
;
[
(
LAp
A
)
,
(
UAp
A
)
]
in
[:
(
bool
the
carrier
of
X
)
,
(
bool
the
carrier
of
X
)
:]
by
ZFMISC_1:87
;
hence
[
(
[#]
X
)
,
(
[#]
X
)
]
is
RoughSet
of
X
by
Def13
,
A1
;
:: thesis:
verum