set OH = OpenHypercubes e;
deffunc H1( Nat) -> Element of bool the carrier of (TopSpaceMetr (Euclid n)) = OpenHypercube (e,(1 / n));
defpred S1[ Nat] means n <> 0 ;
A1: { H1(n) where n is Nat : S1[n] } is countable from CARD_4:sch 1();
 { H1(n) where n is Nat : S1[n] } = OpenHypercubes e
proof
thus { H1(n) where n is Nat : S1[n] } c= OpenHypercubes e :: according to XBOOLE_0:def 10 :: thesis: OpenHypercubes e c= { H1(n) where n is Nat : S1[n] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(n) where n is Nat : S1[n] } or x in OpenHypercubes e )
assume x in { H1(n) where n is Nat : S1[n] } ; :: thesis: x in OpenHypercubes e
then consider n0 being Nat such that
A3: x = H1(n0) and
A4: S1[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 { H1(n) where n is Nat : S1[n] } )
assume x in OpenHypercubes e ; :: thesis: x in { H1(n) where n is Nat : S1[n] }
then consider m0 being non zero Element of NAT such that
A5: x = OpenHypercube (e,(1 / m0)) ;
thus x in { H1(n) where n is Nat : S1[n] } by A5; :: thesis: verum
end;
hence OpenHypercubes e is countable by A1; :: thesis: verum