A1: the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;
reconsider A = RAT as Subset of Sorgenfrey-line by NUMBERS:12, TOPGEN_3:def 2;
consider B being Subset-Family of REAL such that
A2: the topology of Sorgenfrey-line = UniCl B and
A3: B = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } by TOPGEN_3:def 2;
A4: B is Basis of Sorgenfrey-line by A1, A2, 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 set ; :: 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

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
A5: ( C = [.y,q.[ & y < q & q is rational ) by A3;
consider r being rational set such that
A6: ( y < r & r < q ) by A5, RAT_1:22;
assume x in C ; :: thesis: A meets C
( r in A & r in C ) by A5, A6, RAT_1:def 2, XXREAL_1:3;
hence A meets C by XBOOLE_0:3; :: thesis: verum

end;

hence x in Cl A by A4, YELLOW_9:37; :: thesis: verum

end;

hence RAT is dense Subset of Sorgenfrey-line ; :: thesis: verum