From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 12 Mar 2012 14:51:27 +0000 (+0000)
Subject: simple commit foreign inclusion use simple foreign inclusion
X-Git-Tag: f0.2~53
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=3064ca6a757bfdabbc11f78e579dae2f36146bf4;ds=sidebyside

simple commit foreign inclusion use simple foreign inclusion
---

diff --git a/article.tex b/article.tex
index 3f066dc..b4035dd 100644
--- a/article.tex
+++ b/article.tex
@@ -470,10 +470,9 @@ So:
 \[ A \nothaspatch P \implies C \nothaspatch P \]
 $\qed$
 
-\subsection{Foreign inclusion:}
+\subsection{Foreign Inclusion:}
 
-If $D = C$, trivial.  For $D \neq C$:
-$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
+Simple Foreign Inclusion applies.  $\qed$
 
 \subsection{Foreign Contents:}