defpred S1[ 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 S1[y] )
from SUBSET_1:sch 3();
reconsider T = TopStruct(# (product (NAT --> {0,1})),(UniCl (FinMeetCl Y)) #) as non empty strict TopSpace by Th15;
take
T
; ( 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})
; 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 Th18;
take
Y
; 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; verum