set OH = OpenHypercubes e;
deffunc H₁( Nat) -> Element of bool the carrier of (TopSpaceMetr (Euclid n)) = OpenHypercube (e,(1 / n));
defpred S₁[ Nat] means n <> 0 ;
A1: { H₁(n) where n is Nat : S₁[n] } is countable from CARD_4:sch 1();
{ H₁(n) where n is Nat : S₁[n] } = OpenHypercubes e

proof

thus { H₁(n) where n is Nat : S₁[n] } c= OpenHypercubes e :: according to XBOOLE_0:def 10 :: thesis: OpenHypercubes e c= { H₁(n) where n is Nat : S₁[n] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(n) where n is Nat : S₁[n] } or x in OpenHypercubes e )
assume x in { H₁(n) where n is Nat : S₁[n] } ; :: thesis: x in OpenHypercubes e
then consider n0 being Nat such that
A3: x = H₁(n0) and
A4: S₁[n0] ;
n0 is non zero Element of NAT by A4, ORDINAL1:def 12;
hence x in OpenHypercubes e by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHypercubes e or x in { H₁(n) where n is Nat : S₁[n] } )
assume x in OpenHypercubes e ; :: thesis: x in { H₁(n) where n is Nat : S₁[n] }
then consider m0 being non zero Element of NAT such that
A5: x = OpenHypercube (e,(1 / m0)) ;
thus x in { H₁(n) where n is Nat : S₁[n] } by A5; :: thesis: verum

end;

hence OpenHypercubes e is countable by A1; :: thesis: verum