let n be Nat; :: thesis: dense_countable_OpenHypercubes n = { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n }
now :: thesis: for x being object holds
( ( x in dense_countable_OpenHypercubes n implies x in { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n } ) & ( x in { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n } implies x in dense_countable_OpenHypercubes n ) )
let x be object ; :: thesis: ( ( x in dense_countable_OpenHypercubes n implies x in { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n } ) & ( x in { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n } implies x in dense_countable_OpenHypercubes n ) )
hereby :: thesis: ( x in { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n } implies x in dense_countable_OpenHypercubes n )
assume x in dense_countable_OpenHypercubes n ; :: thesis: x in { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n }
then consider y being set such that
A1: x in y and
A2: y in OpenHypercubesRAT n by TARSKI:def 4;
consider z being Point of (Euclid n) such that
A3: y = OpenHypercubes z and
A4: z in RAT n by A2;
consider m being non zero Element of NAT such that
A5: x = OpenHypercube (z,(1 / m)) by A1, A3;
thus x in { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n } by A4, A5; :: thesis: verum
end;
assume x in { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n } ; :: thesis: x in dense_countable_OpenHypercubes n
then consider q0 being Point of (Euclid n), m0 being positive Nat such that
A6: x = OpenHypercube (q0,(1 / m0)) and
A7: q0 in RAT n ;
reconsider p = q0 as Point of (Euclid n) ;
reconsider m1 = m0 as non zero Element of NAT by ORDINAL1:def 12;
OpenHypercube (q0,(1 / m0)) = OpenHypercube (q0,(1 / m1)) ;
then ( x in OpenHypercubes p & OpenHypercubes p in OpenHypercubesRAT n ) by A6, A7;
hence x in dense_countable_OpenHypercubes n by TARSKI:def 4; :: thesis: verum
end;
hence dense_countable_OpenHypercubes n = { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n } by TARSKI:2; :: thesis: verum