reconsider A = RAT as Subset of Sorgenfrey-line by NUMBERS:12, TOPGEN_3:def 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;
the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;
then A3: B is Basis of Sorgenfrey-line by A1, YELLOW_9:22;
A is dense
proof
thus Cl A c= the carrier of Sorgenfrey-line ; :: according to XBOOLE_0:def 10,TOPS_3:def 2 :: thesis: the carrier of Sorgenfrey-line c= Cl A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of Sorgenfrey-line or x in Cl A )
assume x in the carrier of Sorgenfrey-line ; :: thesis: x in Cl A
then reconsider x = x as Point of Sorgenfrey-line ;
now :: thesis: for C being Subset of Sorgenfrey-line st C in B & x in C holds
A meets C
let C be Subset of Sorgenfrey-line; :: thesis: ( C in B & x in C implies A meets C )
assume C in B ; :: thesis: ( x in C implies A meets C )
then consider y, q being Real such that
A4: C = [.y,q.[ and
A5: y < q and
q is rational by A2;
assume x in C ; :: thesis: A meets C
consider r being Rational such that
A6: y < r and
A7: r < q by A5, RAT_1:7;
A8: r in A by RAT_1:def 2;
r in C by A4, A6, A7, XXREAL_1:3;
hence A meets C by A8, XBOOLE_0:3; :: thesis: verum
end;
hence x in Cl A by A3, YELLOW_9:37; :: thesis: verum
end;
hence RAT is dense Subset of Sorgenfrey-line ; :: thesis: verum