let n be Nat; :: thesis: for O being non empty open Subset of (TOP-REAL n) ex p being Element of RAT n st p in O
let O be non empty open Subset of (TOP-REAL n); :: thesis: ex p being Element of RAT n st p in O
RAT n is dense Subset of (TOP-REAL n) by Th15;
then O meets RAT n by TOPS_1:45;
then consider x being object such that
A1: x in O and
A2: x in RAT n by XBOOLE_0:3;
reconsider x = x as Element of RAT n by A2;
take x ; :: thesis: x in O
thus x in O by A1; :: thesis: verum