set T = Sorgenfrey-line ;

consider B being Subset-Family of REAL such that

A1: the topology of Sorgenfrey-line = UniCl B and

A2: B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } by TOPGEN_3:def 2;

let x, y be Point of Sorgenfrey-line; :: according to PRE_TOPC:def 10 :: thesis: ( x = y or ex b_{1}, b_{2} being Element of bool the carrier of Sorgenfrey-line st

( b_{1} is open & b_{2} is open & x in b_{1} & y in b_{2} & b_{1} misses b_{2} ) )

reconsider a = x, b = y as Element of REAL by TOPGEN_3:def 2;

A3: B c= the topology of Sorgenfrey-line by A1, CANTOR_1:1;

assume A4: x <> y ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of Sorgenfrey-line st

( b_{1} is open & b_{2} is open & x in b_{1} & y in b_{2} & b_{1} misses b_{2} )

consider B being Subset-Family of REAL such that

A1: the topology of Sorgenfrey-line = UniCl B and

A2: B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } by TOPGEN_3:def 2;

let x, y be Point of Sorgenfrey-line; :: according to PRE_TOPC:def 10 :: thesis: ( x = y or ex b

( b

reconsider a = x, b = y as Element of REAL by TOPGEN_3:def 2;

A3: B c= the topology of Sorgenfrey-line by A1, CANTOR_1:1;

assume A4: x <> y ; :: thesis: ex b

( b

per cases
( a < b or a > b )
by A4, XXREAL_0:1;

end;

suppose A5:
a < b
; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of Sorgenfrey-line st

( b_{1} is open & b_{2} is open & x in b_{1} & y in b_{2} & b_{1} misses b_{2} )

( b

consider q being Rational such that

A6: b < q and

q < b + 1 by RAT_1:7, XREAL_1:29;

[.b,q.[ in B by A2, A6;

then A7: [.b,q.[ in the topology of Sorgenfrey-line by A3;

consider w being Rational such that

A8: a < w and

A9: w < b by A5, RAT_1:7;

[.a,w.[ in B by A2, A8;

then [.a,w.[ in the topology of Sorgenfrey-line by A3;

then reconsider U = [.a,w.[, V = [.b,q.[ as open Subset of Sorgenfrey-line by A7, PRE_TOPC:def 2;

take U ; :: thesis: ex b_{1} being Element of bool the carrier of Sorgenfrey-line st

( U is open & b_{1} is open & x in U & y in b_{1} & U misses b_{1} )

take V ; :: thesis: ( U is open & V is open & x in U & y in V & U misses V )

A10: U /\ V = {}

thus ( x in U & y in V & U misses V ) by A6, A8, XXREAL_1:3, A10, XBOOLE_0:def 7; :: thesis: verum

end;A6: b < q and

q < b + 1 by RAT_1:7, XREAL_1:29;

[.b,q.[ in B by A2, A6;

then A7: [.b,q.[ in the topology of Sorgenfrey-line by A3;

consider w being Rational such that

A8: a < w and

A9: w < b by A5, RAT_1:7;

[.a,w.[ in B by A2, A8;

then [.a,w.[ in the topology of Sorgenfrey-line by A3;

then reconsider U = [.a,w.[, V = [.b,q.[ as open Subset of Sorgenfrey-line by A7, PRE_TOPC:def 2;

take U ; :: thesis: ex b

( U is open & b

take V ; :: thesis: ( U is open & V is open & x in U & y in V & U misses V )

A10: U /\ V = {}

proof

thus
( U is open & V is open )
; :: thesis: ( x in U & y in V & U misses V )
thus
U /\ V c= {}
:: according to XBOOLE_0:def 10 :: thesis: {} c= U /\ V

end;proof

thus
{} c= U /\ V
by XBOOLE_1:2; :: thesis: verum
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in U /\ V or p in {} )

assume A11: p in U /\ V ; :: thesis: p in {}

then reconsider d = p as ExtReal ;

( d in [.a,w.[ & d in [.b,q.[ ) by XBOOLE_0:def 4, A11;

then ( d < w & b <= d ) by XXREAL_1:3;

hence p in {} by A9, XXREAL_0:2; :: thesis: verum

end;assume A11: p in U /\ V ; :: thesis: p in {}

then reconsider d = p as ExtReal ;

( d in [.a,w.[ & d in [.b,q.[ ) by XBOOLE_0:def 4, A11;

then ( d < w & b <= d ) by XXREAL_1:3;

hence p in {} by A9, XXREAL_0:2; :: thesis: verum

thus ( x in U & y in V & U misses V ) by A6, A8, XXREAL_1:3, A10, XBOOLE_0:def 7; :: thesis: verum

suppose A12:
a > b
; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of Sorgenfrey-line st

( b_{1} is open & b_{2} is open & x in b_{1} & y in b_{2} & b_{1} misses b_{2} )

( b

consider q being Rational such that

A13: a < q and

q < a + 1 by RAT_1:7, XREAL_1:29;

[.a,q.[ in B by A2, A13;

then A14: [.a,q.[ in the topology of Sorgenfrey-line by A3;

consider w being Rational such that

A15: b < w and

A16: w < a by A12, RAT_1:7;

[.b,w.[ in B by A2, A15;

then [.b,w.[ in the topology of Sorgenfrey-line by A3;

then reconsider V = [.b,w.[, U = [.a,q.[ as open Subset of Sorgenfrey-line by A14, PRE_TOPC:def 2;

take U ; :: thesis: ex b_{1} being Element of bool the carrier of Sorgenfrey-line st

( U is open & b_{1} is open & x in U & y in b_{1} & U misses b_{1} )

take V ; :: thesis: ( U is open & V is open & x in U & y in V & U misses V )

A17: U /\ V = {}

thus ( x in U & y in V & U misses V ) by A15, A13, XXREAL_1:3, A17, XBOOLE_0:def 7; :: thesis: verum

end;A13: a < q and

q < a + 1 by RAT_1:7, XREAL_1:29;

[.a,q.[ in B by A2, A13;

then A14: [.a,q.[ in the topology of Sorgenfrey-line by A3;

consider w being Rational such that

A15: b < w and

A16: w < a by A12, RAT_1:7;

[.b,w.[ in B by A2, A15;

then [.b,w.[ in the topology of Sorgenfrey-line by A3;

then reconsider V = [.b,w.[, U = [.a,q.[ as open Subset of Sorgenfrey-line by A14, PRE_TOPC:def 2;

take U ; :: thesis: ex b

( U is open & b

take V ; :: thesis: ( U is open & V is open & x in U & y in V & U misses V )

A17: U /\ V = {}

proof

thus
( U is open & V is open )
; :: thesis: ( x in U & y in V & U misses V )
thus
U /\ V c= {}
:: according to XBOOLE_0:def 10 :: thesis: {} c= U /\ V

end;proof

thus
{} c= U /\ V
:: thesis: verum
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in U /\ V or p in {} )

assume A18: p in U /\ V ; :: thesis: p in {}

then reconsider d = p as ExtReal ;

( d in [.a,q.[ & d in [.b,w.[ ) by XBOOLE_0:def 4, A18;

then ( d < w & a <= d ) by XXREAL_1:3;

hence p in {} by A16, XXREAL_0:2; :: thesis: verum

end;assume A18: p in U /\ V ; :: thesis: p in {}

then reconsider d = p as ExtReal ;

( d in [.a,q.[ & d in [.b,w.[ ) by XBOOLE_0:def 4, A18;

then ( d < w & a <= d ) by XXREAL_1:3;

hence p in {} by A16, XXREAL_0:2; :: thesis: verum

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in {} or p in U /\ V )

assume p in {} ; :: thesis: p in U /\ V

hence p in U /\ V ; :: thesis: verum

end;assume p in {} ; :: thesis: p in U /\ V

hence p in U /\ V ; :: thesis: verum

thus ( x in U & y in V & U misses V ) by A15, A13, XXREAL_1:3, A17, XBOOLE_0:def 7; :: thesis: verum