:: deftheorem defines <. CARDFIL2:def 12 :
for X being non empty set
for B being filter_base of X holds <.B.) = <.B.];