let X be non empty TopSpace; for Y being monotone-convergence T_0-TopSpace holds ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
let Y be monotone-convergence T_0-TopSpace; ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
set L = (Omega Y) |^ the carrier of X;
reconsider C = ContMaps (X,(Omega Y)) as non empty full SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;
C is directed-sups-inheriting
proof
let D be
directed Subset of
C;
WAYBEL_0:def 4 ( D = {} or not ex_sup_of D,(Omega Y) |^ the carrier of X or "\/" (D,((Omega Y) |^ the carrier of X)) in the carrier of C )
assume that A1:
D <> {}
and
ex_sup_of D,
(Omega Y) |^ the
carrier of
X
;
"\/" (D,((Omega Y) |^ the carrier of X)) in the carrier of C
reconsider D =
D as non
empty directed Subset of
C by A1;
set N =
Net-Str D;
A2:
TopStruct(# the
carrier of
X, the
topology of
X #)
= TopStruct(# the
carrier of
X, the
topology of
X #)
;
for
x being
Point of
X holds
commute (
(Net-Str D),
x,
(Omega Y)) is
eventually-directed
;
then A3:
"\/" (
(rng the mapping of (Net-Str D)),
((Omega Y) |^ the carrier of X)) is
continuous Function of
X,
Y
by Th42;
TopStruct(# the
carrier of
Y, the
topology of
Y #)
= TopStruct(# the
carrier of
(Omega Y), the
topology of
(Omega Y) #)
by Def2;
then
"\/" (
(rng the mapping of (Net-Str D)),
((Omega Y) |^ the carrier of X)) is
continuous Function of
X,
(Omega Y)
by A2, A3, YELLOW12:36;
then A4:
"\/" (
(rng the mapping of (Net-Str D)),
((Omega Y) |^ the carrier of X))
in the
carrier of
C
by WAYBEL24:def 3;
Net-Str D = NetStr(#
D,
( the InternalRel of C |_2 D),
((id the carrier of C) | D) #)
by WAYBEL17:def 4;
hence
"\/" (
D,
((Omega Y) |^ the carrier of X))
in the
carrier of
C
by A4, YELLOW14:2;
verum
end;
hence
ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
; verum