chiark / gitweb /
simple commit foreign inclusion use simple foreign inclusion
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 14:51:27 +0000 (14:51 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 14:51:27 +0000 (14:51 +0000)
article.tex

index 3f066dc..b4035dd 100644 (file)
@@ -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:}