let X be non empty TopSpace; :: thesis: for Y being non trivial T_0-TopSpace st oContMaps (X,Y) is with_suprema holds

not Y is T_1

let Y be non trivial T_0-TopSpace; :: thesis: ( oContMaps (X,Y) is with_suprema implies not Y is T_1 )

consider a, b being Element of Y such that

A1: a <> b by STRUCT_0:def 10;

set i = the Element of X;

reconsider f = X --> a, g = X --> b as continuous Function of X,Y ;

assume oContMaps (X,Y) is with_suprema ; :: thesis: not Y is T_1

then reconsider XY = oContMaps (X,Y) as sup-Semilattice ;

reconsider ef = f, eg = g as Element of XY by Th2;

reconsider h = ef "\/" eg, f = ef, g = eg as continuous Function of X,(Omega Y) by Th1;

A2: ( f . the Element of X = a & g . the Element of X = b ) by FUNCOP_1:7;

A6: x <= y and

A7: x <> y ;

A8: TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) by WAYBEL25:def 2;

then reconsider p = x, q = y as Element of Y ;

take p ; :: according to URYSOHN1:def 7 :: thesis: ex b_{1} being Element of the carrier of Y st

( not p = b_{1} & ( for b_{2}, b_{3} being Element of bool the carrier of Y holds

( not b_{2} is open or not b_{3} is open or not p in b_{2} or b_{1} in b_{2} or not b_{1} in b_{3} or p in b_{3} ) ) )

take q ; :: thesis: ( not p = q & ( for b_{1}, b_{2} being Element of bool the carrier of Y holds

( not b_{1} is open or not b_{2} is open or not p in b_{1} or q in b_{1} or not q in b_{2} or p in b_{2} ) ) )

thus p <> q by A7; :: thesis: for b_{1}, b_{2} being Element of bool the carrier of Y holds

( not b_{1} is open or not b_{2} is open or not p in b_{1} or q in b_{1} or not q in b_{2} or p in b_{2} )

let W, V be Subset of Y; :: thesis: ( not W is open or not V is open or not p in W or q in W or not q in V or p in V )

assume W is open ; :: thesis: ( not V is open or not p in W or q in W or not q in V or p in V )

then reconsider W = W as open Subset of (Omega Y) by A8, TOPS_3:76;

W is upper ;

hence ( not V is open or not p in W or q in W or not q in V or p in V ) by A6; :: thesis: verum

not Y is T_1

let Y be non trivial T_0-TopSpace; :: thesis: ( oContMaps (X,Y) is with_suprema implies not Y is T_1 )

consider a, b being Element of Y such that

A1: a <> b by STRUCT_0:def 10;

set i = the Element of X;

reconsider f = X --> a, g = X --> b as continuous Function of X,Y ;

assume oContMaps (X,Y) is with_suprema ; :: thesis: not Y is T_1

then reconsider XY = oContMaps (X,Y) as sup-Semilattice ;

reconsider ef = f, eg = g as Element of XY by Th2;

reconsider h = ef "\/" eg, f = ef, g = eg as continuous Function of X,(Omega Y) by Th1;

A2: ( f . the Element of X = a & g . the Element of X = b ) by FUNCOP_1:7;

now :: thesis: ex x, y being Element of (Omega Y) st

( x <= y & x <> y )

then consider x, y being Element of (Omega Y) such that ( x <= y & x <> y )

eg <= ef "\/" eg
by YELLOW_0:22;

then g <= h by Th3;

then A3: ex x, y being Element of (Omega Y) st

( x = g . the Element of X & y = h . the Element of X & x <= y ) ;

ef <= ef "\/" eg by YELLOW_0:22;

then f <= h by Th3;

then A4: ex x, y being Element of (Omega Y) st

( x = f . the Element of X & y = h . the Element of X & x <= y ) ;

assume A5: for x, y being Element of (Omega Y) holds

( not x <= y or not x <> y ) ; :: thesis: contradiction

then ( not f . the Element of X <= h . the Element of X or not f . the Element of X <> h . the Element of X ) ;

hence contradiction by A1, A2, A5, A4, A3; :: thesis: verum

end;then g <= h by Th3;

then A3: ex x, y being Element of (Omega Y) st

( x = g . the Element of X & y = h . the Element of X & x <= y ) ;

ef <= ef "\/" eg by YELLOW_0:22;

then f <= h by Th3;

then A4: ex x, y being Element of (Omega Y) st

( x = f . the Element of X & y = h . the Element of X & x <= y ) ;

assume A5: for x, y being Element of (Omega Y) holds

( not x <= y or not x <> y ) ; :: thesis: contradiction

then ( not f . the Element of X <= h . the Element of X or not f . the Element of X <> h . the Element of X ) ;

hence contradiction by A1, A2, A5, A4, A3; :: thesis: verum

A6: x <= y and

A7: x <> y ;

A8: TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) by WAYBEL25:def 2;

then reconsider p = x, q = y as Element of Y ;

take p ; :: according to URYSOHN1:def 7 :: thesis: ex b

( not p = b

( not b

take q ; :: thesis: ( not p = q & ( for b

( not b

thus p <> q by A7; :: thesis: for b

( not b

let W, V be Subset of Y; :: thesis: ( not W is open or not V is open or not p in W or q in W or not q in V or p in V )

assume W is open ; :: thesis: ( not V is open or not p in W or q in W or not q in V or p in V )

then reconsider W = W as open Subset of (Omega Y) by A8, TOPS_3:76;

W is upper ;

hence ( not V is open or not p in W or q in W or not q in V or p in V ) by A6; :: thesis: verum