card [:BE,BK:] is finite ;
then card (Base (BE,BK)) is finite by BE1;
hence Base (BE,BK) is finite ; :: thesis: verum