defpred S₁[ set ] means ex N, n being Nat st
for F being Element of product (NAT --> {0 ,1}) holds
( F in $1 iff F . N = n );
consider Y being Subset-Family of (product (NAT --> {0 ,1})) such that
A1: for y being Subset of (product (NAT --> {0 ,1})) holds
( y in Y iff S₁[y] ) from SUBSET_1:sch 3();
reconsider T = TopStruct(# (product (NAT --> {0 ,1})),(UniCl (FinMeetCl Y)) #) as non empty strict TopSpace by Th17;
take T ; :: thesis: ( the carrier of T = product (NAT --> {0 ,1}) & ex P being prebasis of T 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 ) ) )
thus the carrier of T = product (NAT --> {0 ,1}) ; :: thesis: ex P being prebasis of T 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 ) )
reconsider Y = Y as prebasis of T by Th20;
take Y ; :: thesis: for X being Subset of (product (NAT --> {0 ,1})) holds
( X in Y iff ex N, n being Nat st
for F being Element of product (NAT --> {0 ,1}) holds
( F in X iff F . N = n ) )
thus for X being Subset of (product (NAT --> {0 ,1})) holds
( X in Y iff ex N, n being Nat st
for F being Element of product (NAT --> {0 ,1}) holds
( F in X iff F . N = n ) ) by A1; :: thesis: verum