:: deftheorem defines the_Cantor_set CANTOR_1:def 5 :
for b₁ being non empty strict TopSpace holds
( b₁ = the_Cantor_set iff ( the carrier of b₁ = product (NAT --> {0,1}) & ex P being prebasis of b₁ st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) ) );