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

proof

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;

then reconsider C = [:RAT,RAT:] as Subset of Sorgenfrey-plane ;
for A being Subset of Sorgenfrey-plane st A <> {} & A is open holds
A meets C

proof

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;

now :: thesis: ex e being set st
( e in B & not e = {} )

assume A7: for e being set st e in B holds
e = {} ; :: thesis: contradiction
union B c= {}

proof

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;

hence contradiction by A5, A3; :: thesis: verum

end;

then consider e being set such that
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;

hence [:RAT,RAT:] is dense Subset of Sorgenfrey-plane by TOPS_1:45; :: thesis: verum