let
Y
be non
empty
TopStruct
;
:: thesis:
for
A
being non
empty
Subset
of
Y
holds
A
is
Subset
of
(
Sspace
A
)
let
A
be non
empty
Subset
of
Y
;
:: thesis:
A
is
Subset
of
(
Sspace
A
)
the
carrier
of
(
Sspace
A
)
c=
the
carrier
of
(
Sspace
A
)
;
hence
A
is
Subset
of
(
Sspace
A
)
by
Lm3
;
:: thesis:
verum