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