theorem Th44: :: CARDFIL2:94

for T being non empty TopSpace
for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( ( for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) iff for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b )