let n be Nat; :: thesis: OpenHypercubesRAT n is countable
deffunc H₁( object ) -> Element of bool (bool the carrier of (TopSpaceMetr (Euclid n))) = OpenHypercubes (@ (object2RAT ($1,n)));
consider ff being Function such that
A1: dom ff = RAT n and
A2: for x being object st x in RAT n holds
ff . x = H₁(x) from FUNCT_1:sch 3();
A3: OpenHypercubesRAT n = rng ff

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: rng ff c= OpenHypercubesRAT n

let x be object ; :: thesis: ( x in OpenHypercubesRAT n implies x in rng ff )
assume x in OpenHypercubesRAT n ; :: thesis: x in rng ff
then consider q0 being Point of (Euclid n) such that
A4: x = OpenHypercubes q0 and
A5: q0 in RAT n ;
x = ff . q0

proof

ff . q0 = H₁(q0) by A5, A2;
hence x = ff . q0 by A4, A5, Def1; :: thesis: verum

end;

hence x in rng ff by A5, A1, FUNCT_1:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ff or x in OpenHypercubesRAT n )
assume x in rng ff ; :: thesis: x in OpenHypercubesRAT n
then consider q0 being object such that
A6: q0 in dom ff and
A7: x = ff . q0 by FUNCT_1:def 3;
( RAT n c= REAL n & q0 in RAT n ) by NUMBERS:12, Th5, A6, A1;
then reconsider q1 = q0 as Point of (Euclid n) ;
ff . q1 = H₁(q0) by A6, A1, A2;
hence x in OpenHypercubesRAT n by A7; :: thesis: verum

end;

card (rng ff) c= card (dom ff) by CARD_2:61;
hence OpenHypercubesRAT n is countable by A3, A1, WAYBEL12:1; :: thesis: verum