H1(n,e) c= bool the carrier of (TopSpaceMetr (Euclid n))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(n,e) or x in bool the carrier of (TopSpaceMetr (Euclid n)) )
assume x in H1(n,e) ; :: thesis: x in bool the carrier of (TopSpaceMetr (Euclid n))
then ex m being non zero Element of NAT st x = OpenHypercube (e,(1 / m)) ;
hence x in bool the carrier of (TopSpaceMetr (Euclid n)) by ZFMISC_1:def 1; :: thesis: verum
end;
hence { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } is Subset-Family of (TopSpaceMetr (Euclid n)) ; :: thesis: verum