len (SubXFinS f,{} ) = card {} by AC200;
hence SubXFinS f,{} is empty ; :: thesis: verum