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,() 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 () 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 () 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 () st
( x = f . the Element of X & y = h . the Element of X & x <= y ) ;
assume A5: for x, y being Element of () 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 () such that
A6: x <= y and
A7: x <> y ;
A8: TopStruct(# the carrier of (), the topology of () #) = 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 b1 being Element of the carrier of Y st
( not p = b1 & ( for b2, b3 being Element of bool the carrier of Y holds
( not b2 is open or not b3 is open or not p in b2 or b1 in b2 or not b1 in b3 or p in b3 ) ) )

take q ; :: thesis: ( not p = q & ( for b1, b2 being Element of bool the carrier of Y holds
( not b1 is open or not b2 is open or not p in b1 or q in b1 or not q in b2 or p in b2 ) ) )

thus p <> q by A7; :: thesis: for b1, b2 being Element of bool the carrier of Y holds
( not b1 is open or not b2 is open or not p in b1 or q in b1 or not q in b2 or p in b2 )

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 () by ;
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