[#]
Y
=
the
carrier
of
Y
;
then
reconsider
A0
= the
carrier
of
Y
as non
empty
Subset
of
Y
;
set
Y0
=
Y

A0
;
take
Y

A0
;
:: thesis:
( not
Y

A0
is
proper
&
Y

A0
is
strict
)
A0
=
[#]
(
Y

A0
)
by
PRE_TOPC:def 5
;
hence
( not
Y

A0
is
proper
&
Y

A0
is
strict
)
by
TEX_2:10
;
:: thesis:
verum