let n be Nat; :: thesis:
RAT n is Subset of (REAL n) by NUMBERS:12, Th5;
then reconsider RATN = RAT n as Subset of (TOP-REAL n) by EUCLID:22;
for Q being Subset of (TOP-REAL n) st Q <> {} & Q is open holds
RATN meets Q

let Q be Subset of (TOP-REAL n); :: thesis:
assume that
A1: Q <> {} and
A2: Q is open ; :: thesis:
consider q being object such that
A3: q in Q by A1, XBOOLE_0:def 1;
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider Q0 = Q as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider q0 = q as Point of (Euclid n) by A3, EUCLID:67;
Q0 is open by A2, Th10;
then consider m being non zero Element of NAT such that
A6: OpenHypercube (q0,(1 / m)) c= Q0 by A3, EUCLID_9:23;
set OH = OpenHypercube (q0,(1 / m));
set f = Intervals (q0,(1 / m));
A7: dom (Intervals (q0,(1 / m))) = dom q0 by EUCLID_9:def 3;
A8: for x being object st x in dom (Intervals (q0,(1 / m))) holds
ex k being Element of RAT st k in (Intervals (q0,(1 / m))) . x

let x be object ; :: thesis:
assume A9: x in dom (Intervals (q0,(1 / m))) ; :: thesis:
reconsider FF = ].((q0 . x) - (1 / m)),((q0 . x) + (1 / m)).[ as open Subset of R^1 by BORSUK_5:39;
A10: (q0 . x) - (1 / m) < q0 . x by XREAL_1:44;
q0 . x < (q0 . x) + (1 / m) by XREAL_1:29;
then (q0 . x) - (1 / m) < (q0 . x) + (1 / m) by A10, XXREAL_0:2;
then ( FF <> {} & FF is open ) by XXREAL_1:33;
then FF meets RAT by TOPGEN_1:51, TOPS_1:45;
then consider k being object such that
A11: ( k in FF & k in RAT ) by XBOOLE_0:3;
take k ; :: thesis:
thus ( k is set & k is Element of RAT & k in (Intervals (q0,(1 / m))) . x ) by A11, A9, A7, EUCLID_9:def 3; :: thesis:

end;

q in TOP-REAL n by A3;
then q in REAL n by EUCLID:22;
then reconsider q1 = q as FinSequence of REAL by FINSEQ_2:131;
A12: dom q1 = Seg n by A3, FINSEQ_1:89;
defpred S₁[ object , object ] means ( $2 in (Intervals (q0,(1 / m))) . $1 & $2 is Element of RAT );
A13: for x being Nat st x in Seg n holds
ex y being object st S₁[x,y]

let x be Nat; :: thesis:
assume x in Seg n ; :: thesis:
then consider k being Element of RAT such that
A14: k in (Intervals (q0,(1 / m))) . x by A8, A7, A12;
take k ; :: thesis:
thus S₁[x,k] by A14; :: thesis:

end;

end;

rng p c= RAT

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng p ; :: thesis:
then consider x0 being object such that
A18: x0 in dom p and
A19: x = p . x0 by FUNCT_1:def 3;
( p . x0 in (Intervals (q0,(1 / m))) . x0 & p . x0 is Element of RAT ) by A16, A18, A15;
hence x in RAT by A19; :: thesis:

end;

end;

end;

end;

end;

end;

end;