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 b1, b2 being Element of bool the carrier of Sorgenfrey-line st
( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 ) )
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 b1, b2 being Element of bool the carrier of Sorgenfrey-line st
( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 )
per cases ( a < b or a > b ) by A4, XXREAL_0:1;
suppose A5: a < b ; :: thesis: ex b1, b2 being Element of bool the carrier of Sorgenfrey-line st
( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 )
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 b1 being Element of bool the carrier of Sorgenfrey-line st
( U is open & b1 is open & x in U & y in b1 & U misses b1 )
take V ; :: thesis: ( U is open & V is open & x in U & y in V & U misses V )
A10: U /\ V = {}
proof
thus U /\ V c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= U /\ V
proof
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;
thus {} c= U /\ V by XBOOLE_1:2; :: thesis: verum
end;
thus ( U is open & V is open ) ; :: thesis: ( x in U & y in V & U misses 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;
suppose A12: a > b ; :: thesis: ex b1, b2 being Element of bool the carrier of Sorgenfrey-line st
( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 )
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 b1 being Element of bool the carrier of Sorgenfrey-line st
( U is open & b1 is open & x in U & y in b1 & U misses b1 )
take V ; :: thesis: ( U is open & V is open & x in U & y in V & U misses V )
A17: U /\ V = {}
proof
thus U /\ V c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= U /\ V
proof
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;
thus {} c= U /\ V :: 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;
end;
thus ( U is open & V is open ) ; :: thesis: ( x in U & y in V & U misses 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;
end;