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