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;
assume oContMaps X,Y is with_suprema ; :: thesis: not Y is T_1
then reconsider XY = oContMaps X,Y as sup-Semilattice ;
reconsider f = X --> a, g = X --> b as continuous Function of X,Y ;
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;
consider i being Element of X;
A2: ( f . i = a & g . i = b ) by FUNCOP_1:13;

now

assume for x, y being Element of (Omega Y) holds
( not x <= y or not x <> y ) ; :: thesis: contradiction
then A3: ( ( not f . i <= h . i or not f . i <> h . i ) & ( not g . i <= h . i or not g . i <> h . i ) ) ;
( ef <= ef "\/" eg & eg <= ef "\/" eg ) by YELLOW_0:22;
then ( f <= h & g <= h ) by Th3;
then ( ex x, y being Element of (Omega Y) st
( x = f . i & y = h . i & x <= y ) & ex x, y being Element of (Omega Y) st
( x = g . i & y = h . i & x <= y ) ) by YELLOW_2:def 1;
hence contradiction by A1, A2, A3; :: thesis: verum

end;

then consider x, y being Element of (Omega Y) such that
A4: ( x <= y & x <> y ) ;
A5: 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 9 :: 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 A4; :: 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 A5, 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 A4, WAYBEL_0:def 20; :: thesis: verum