[:RAT,RAT:] c= [#] Sorgenfrey-plane

for A being Subset of Sorgenfrey-plane st A <> {} & A is open holds

A meets C

proof

then reconsider C = [:RAT,RAT:] as Subset of Sorgenfrey-plane ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:RAT,RAT:] or z in [#] Sorgenfrey-plane )

assume z in [:RAT,RAT:] ; :: thesis: z in [#] Sorgenfrey-plane

then consider x, y being object such that

A1: ( x in RAT & y in RAT ) and

A2: z = [x,y] by ZFMISC_1:def 2;

( x in REAL & y in REAL ) by A1, NUMBERS:12;

then ( x in [#] Sorgenfrey-line & y in [#] Sorgenfrey-line ) by TOPGEN_3:def 2;

then z in [:([#] Sorgenfrey-line),([#] Sorgenfrey-line):] by A2, ZFMISC_1:def 2;

hence z in [#] Sorgenfrey-plane ; :: thesis: verum

end;assume z in [:RAT,RAT:] ; :: thesis: z in [#] Sorgenfrey-plane

then consider x, y being object such that

A1: ( x in RAT & y in RAT ) and

A2: z = [x,y] by ZFMISC_1:def 2;

( x in REAL & y in REAL ) by A1, NUMBERS:12;

then ( x in [#] Sorgenfrey-line & y in [#] Sorgenfrey-line ) by TOPGEN_3:def 2;

then z in [:([#] Sorgenfrey-line),([#] Sorgenfrey-line):] by A2, ZFMISC_1:def 2;

hence z in [#] Sorgenfrey-plane ; :: thesis: verum

for A being Subset of Sorgenfrey-plane st A <> {} & A is open holds

A meets C

proof

hence
[:RAT,RAT:] is dense Subset of Sorgenfrey-plane
by TOPS_1:45; :: thesis: verum
let A be Subset of Sorgenfrey-plane; :: thesis: ( A <> {} & A is open implies A meets C )

assume that

A3: A <> {} and

A4: A is open ; :: thesis: A meets C

consider B being Subset-Family of Sorgenfrey-plane such that

A5: A = union B and

A6: for e being set st e in B holds

ex X1, Y1 being Subset of Sorgenfrey-line st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5, A4;

A9: ( e in B & e <> {} ) ;

consider X1, Y1 being Subset of Sorgenfrey-line such that

A10: e = [:X1,Y1:] and

A11: ( X1 is open & Y1 is open ) by A6, A9;

A12: ( X1 <> {} & Y1 <> {} ) by ZFMISC_1:90, A9, A10;

consider x1 being object such that

A13: x1 in X1 by A12, XBOOLE_0:7;

consider y1 being object such that

A14: y1 in Y1 by A12, XBOOLE_0:7;

consider ax being Subset of Sorgenfrey-line such that

A15: ax in BB and

x1 in ax and

A16: ax c= X1 by YELLOW_9:31, A11, A13, Lm8;

consider ay being Subset of Sorgenfrey-line such that

A17: ay in BB and

y1 in ay and

A18: ay c= Y1 by YELLOW_9:31, A11, A14, Lm8;

consider px, qx being Real such that

A19: ax = [.px,qx.[ and

A20: ( px < qx & qx is rational ) by A15, Lm7;

consider py, qy being Real such that

A21: ay = [.py,qy.[ and

A22: ( py < qy & qy is rational ) by A17, Lm7;

consider rx being Rational such that

A23: ( px < rx & rx < qx ) by RAT_1:7, A20;

A24: rx in ax by A23, XXREAL_1:3, A19;

consider ry being Rational such that

A25: ( py < ry & ry < qy ) by RAT_1:7, A22;

A26: ry in ay by A25, XXREAL_1:3, A21;

( rx in RAT & ry in RAT ) by RAT_1:def 2;

then A27: [rx,ry] in C by ZFMISC_1:def 2;

[rx,ry] in [:X1,Y1:] by A24, A26, A16, A18, ZFMISC_1:def 2;

then A28: [rx,ry] in A by A5, A9, A10, TARSKI:def 4;

thus A meets C by A27, A28, XBOOLE_0:3; :: thesis: verum

end;assume that

A3: A <> {} and

A4: A is open ; :: thesis: A meets C

consider B being Subset-Family of Sorgenfrey-plane such that

A5: A = union B and

A6: for e being set st e in B holds

ex X1, Y1 being Subset of Sorgenfrey-line st

( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5, A4;

now :: thesis: ex e being set st

( e in B & not e = {} )

then consider e being set such that ( e in B & not e = {} )

assume A7:
for e being set st e in B holds

e = {} ; :: thesis: contradiction

union B c= {}

end;e = {} ; :: thesis: contradiction

union B c= {}

proof

hence
contradiction
by A5, A3; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union B or z in {} )

assume z in union B ; :: thesis: z in {}

then consider y being set such that

A8: ( z in y & y in B ) by TARSKI:def 4;

thus z in {} by A8, A7; :: thesis: verum

end;assume z in union B ; :: thesis: z in {}

then consider y being set such that

A8: ( z in y & y in B ) by TARSKI:def 4;

thus z in {} by A8, A7; :: thesis: verum

A9: ( e in B & e <> {} ) ;

consider X1, Y1 being Subset of Sorgenfrey-line such that

A10: e = [:X1,Y1:] and

A11: ( X1 is open & Y1 is open ) by A6, A9;

A12: ( X1 <> {} & Y1 <> {} ) by ZFMISC_1:90, A9, A10;

consider x1 being object such that

A13: x1 in X1 by A12, XBOOLE_0:7;

consider y1 being object such that

A14: y1 in Y1 by A12, XBOOLE_0:7;

consider ax being Subset of Sorgenfrey-line such that

A15: ax in BB and

x1 in ax and

A16: ax c= X1 by YELLOW_9:31, A11, A13, Lm8;

consider ay being Subset of Sorgenfrey-line such that

A17: ay in BB and

y1 in ay and

A18: ay c= Y1 by YELLOW_9:31, A11, A14, Lm8;

consider px, qx being Real such that

A19: ax = [.px,qx.[ and

A20: ( px < qx & qx is rational ) by A15, Lm7;

consider py, qy being Real such that

A21: ay = [.py,qy.[ and

A22: ( py < qy & qy is rational ) by A17, Lm7;

consider rx being Rational such that

A23: ( px < rx & rx < qx ) by RAT_1:7, A20;

A24: rx in ax by A23, XXREAL_1:3, A19;

consider ry being Rational such that

A25: ( py < ry & ry < qy ) by RAT_1:7, A22;

A26: ry in ay by A25, XXREAL_1:3, A21;

( rx in RAT & ry in RAT ) by RAT_1:def 2;

then A27: [rx,ry] in C by ZFMISC_1:def 2;

[rx,ry] in [:X1,Y1:] by A24, A26, A16, A18, ZFMISC_1:def 2;

then A28: [rx,ry] in A by A5, A9, A10, TARSKI:def 4;

thus A meets C by A27, A28, XBOOLE_0:3; :: thesis: verum