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