for
i
being
Element
of
A
holds
(
A
-->
R
)
.
i
is
complete
Heyting
LATTICE
;
then
(
product
(
A
-->
R
)
is
complete
&
product
(
A
-->
R
)
is
Heyting
)
by
Th13
;
hence
R
|^
A
is
Heyting
by
YELLOW_1:def 5
;
:: thesis:
verum