set
X1
=
{
(
0.
X
)
}
;
reconsider
X1
=
{
(
0.
X
)
}
as
Ideal
of
X
by
Lm3
;
take
X1
;
:: thesis:
X1
is
closed
for
x
being
Element
of
X1
holds
x
`
in
X1
by
Lm4
;
hence
X1
is
closed
;
:: thesis:
verum