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;

now :: thesis: ex x, y being Element of (Omega Y) st
( 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 consider x, y being Element of (Omega Y) such that
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₁ being Element of the carrier of Y st
( not p = b₁ & ( for b₂, b₃ being Element of bool the carrier of Y holds
( not b₂ is open or not b₃ is open or not p in b₂ or b₁ in b₂ or not b₁ in b₃ or p in b₃ ) ) )
take q ; :: thesis: ( not p = q & ( for b₁, b₂ being Element of bool the carrier of Y holds
( not b₁ is open or not b₂ is open or not p in b₁ or q in b₁ or not q in b₂ or p in b₂ ) ) )
thus p <> q by A7; :: thesis: for b₁, b₂ being Element of bool the carrier of Y holds
( not b₁ is open or not b₂ is open or not p in b₁ or q in b₁ or not q in b₂ or p in 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