X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=pseudomerge.tex;h=c1a88f8c6dc170be2e451902101dcc6ebebb5970;hb=d487ea8f587d3e514a04ee7b99d6d14f27792851;hp=27b2e528525bef39cd8a2bfe8556389cac0ff5c7;hpb=ff4ffb2eb74387bab00f6f7536f1037bb9a9f0aa;p=topbloke-formulae.git

diff --git a/pseudomerge.tex b/pseudomerge.tex
index 27b2e52..c1a88f8 100644
--- a/pseudomerge.tex
+++ b/pseudomerge.tex
@@ -88,7 +88,15 @@ Explicitly dealt with by our Unique Tips condition.
 
 \subsection{Foreign Inclusion}
 
-True by Foreign Identical, and Foreign Inclusion of $L$.
+We need to consider $D \in \foreign$.
+
+For $D = C$: $D \has C$, $D \le C$; OK.
+
+For $D \neq C$: $D \has C \equiv D \has L$ by construction.
+$D \has L \equiv D \le L$ by Foreign Inclusion of $L$.
+$D \neq C$ so this $D \le L \equiv D \le C$.
+
+$\qed$
 
 \subsection{Foreign Ancestry}