H_{1}(n,e) c= bool the carrier of (TopSpaceMetr (Euclid n))

proof

hence
{ (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } is Subset-Family of (TopSpaceMetr (Euclid n))
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{1}(n,e) or x in bool the carrier of (TopSpaceMetr (Euclid n)) )

assume x in H_{1}(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;assume x in H

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