let S be monotone-convergence T_0-TopSpace; for T being T_0-TopSpace st S,T are_homeomorphic holds
T is monotone-convergence
let T be T_0-TopSpace; ( S,T are_homeomorphic implies T is monotone-convergence )
given h being Function of S,T such that A1:
h is being_homeomorphism
; T_0TOPSP:def 1 T is monotone-convergence
the carrier of S = the carrier of (Omega S)
by Lm1;
then reconsider f = h as Function of (Omega S),(Omega T) by Lm1;
f is isomorphic
by A1, Th18;
then A2:
rng f = the carrier of (Omega T)
by WAYBEL_0:66;
let D be non empty directed Subset of (Omega T); WAYBEL25:def 4 ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) )
A3:
f " is isomorphic
by A1, Th18, YELLOW14:10;
then
f " is sups-preserving
by WAYBEL13:20;
then A4:
f " preserves_sup_of D
;
A5:
rng h = [#] T
by A1;
A6:
h is V7()
by A1;
A7:
h is onto
by A5, FUNCT_2:def 3;
(f ") .: D is directed
by A3, YELLOW_2:15;
then A8:
f " D is non empty directed Subset of (Omega S)
by A2, A5, A6, TOPS_2:55;
then
ex_sup_of f " D, Omega S
by Def4;
then
ex_sup_of f .: (f " D), Omega T
by A1, Th18, YELLOW14:16;
hence A9:
ex_sup_of D, Omega T
by A2, FUNCT_1:77; for V being open Subset of T st sup D in V holds
D meets V
let V be open Subset of T; ( sup D in V implies D meets V )
assume
sup D in V
; D meets V
then
(h ") . (sup D) in (h ") .: V
by FUNCT_2:35;
then
(h ") . (sup D) in h " V
by A5, A6, TOPS_2:55;
then
(h ") . (sup D) in h " V
by A7, A6, TOPS_2:def 4;
then
(f ") . (sup D) in h " V
by A2, A6, A7, A5, TOPS_2:def 4;
then
sup ((f ") .: D) in h " V
by A9, A4;
then A10:
sup (f " D) in h " V
by A2, A5, A6, TOPS_2:55;
h " V is open
by A1, TOPGRP_1:26;
then
f " D meets h " V
by A8, A10, Def4;
then consider a being object such that
A11:
a in f " D
and
A12:
a in h " V
by XBOOLE_0:3;
reconsider a = a as Element of S by A12;
hence
D meets V
by XBOOLE_0:3; verum