theorem Th24: :: CARDFIL4:25

for X1 being non empty set
for cF1 being Filter of X1 ex cB1 being filter_base of X1 st <.cB1.) = cF1