theorem Th06: :: CARDFIL2:21
for X being non empty set
for F being Filter of X
for B being basis of F holds F = <.(# B).]