theorem Th07: :: CARDFIL2:22

for X being non empty set
for F being Filter of X
for B being Subset-Family of X st F = <.B.] holds
B is basis of F