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