theorem
Th31
:
:: WAYBEL29:31
for
L
being
complete
LATTICE
holds
( ( for
S
being
complete
LATTICE
holds
sigma
[:
S
,
L
:]
=
the
topology
of
[:
(
Sigma
S
)
,
(
Sigma
L
)
:]
) iff for
S
being
complete
LATTICE
holds
TopStruct
(# the
carrier
of
(
Sigma
[:
S
,
L
:]
)
, the
topology
of
(
Sigma
[:
S
,
L
:]
)
#)
=
[:
(
Sigma
S
)
,
(
Sigma
L
)
:]
)