let X be non empty TopSpace; :: thesis: 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; :: thesis: 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;
:: according to WAYBEL_0:def 4 :: thesis: ( 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
;
:: thesis: "\/" 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
Y,the
topology of
Y #)
= TopStruct(# the
carrier of
(Omega Y),the
topology of
(Omega Y) #)
by Def2;
A3:
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
"\/" (rng the mapping of (Net-Str D)),
((Omega Y) |^ the carrier of X) is
continuous Function of
X,
Y
by Th42;
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;
:: thesis: verum
end;
hence
ContMaps X,(Omega Y) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
; :: thesis: verum