theorem Th08: :: CARDFIL2:25

for X being non empty set
for B being filter_base of X holds <.B.] is Filter of X