reconsider
x
=
x
as
Element
of
INT
by
INT_1:def 2
;
f
.
x
is
Element
of
D
;
hence
f
.
x
is
Element
of
D
;
:: thesis:
verum