let
X
be
set
;
:: thesis:
for
F
being
filtering
Operation
of
X
holds
F
OR
(
NOT
F
)
=
id
X
let
F
be
filtering
Operation
of
X
;
:: thesis:
F
OR
(
NOT
F
)
=
id
X
(
dom
(
F
OR
(
NOT
F
)
)
=
X
&
F
OR
(
NOT
F
)
c=
id
X
)
by
Th50
,
Def21
;
hence
F
OR
(
NOT
F
)
=
id
X
by
SYSREL:17
;
:: thesis:
verum