[
(
(
LAp
A
)
\/
(
LAp
B
)
)
,
(
(
UAp
A
)
\/
(
UAp
B
)
)
]
in
[:
(
bool
the
carrier
of
X
)
,
(
bool
the
carrier
of
X
)
:]
by
ZFMISC_1:87
;
hence
[
(
(
LAp
A
)
\/
(
LAp
B
)
)
,
(
(
UAp
A
)
\/
(
UAp
B
)
)
]
is
RoughSet
of
X
by
Def13
;
:: thesis:
verum