diff --git a/tex/applications.tex b/tex/applications.tex
index 1e3a0813ee5d60d34514ac90279f0dcd766adc55..50d822840b3cce24f340d98c5794cb1deacc6f46 100644
--- a/tex/applications.tex
+++ b/tex/applications.tex
@@ -6,4 +6,7 @@
 - prioritize many definitions / theorems
 - refactoring advice
 - assoc / comm normalization
-- term indexing techniques
\ No newline at end of file
+- term indexing techniques
+- use existing views in $\cL$ (compositions of views are vivews) to give Jane more
+  information about her beautiful subsets, e.g. that matroids (and thus beautiful sets)
+  form a generalization of the notion of linear independence from linear algebra.
\ No newline at end of file
diff --git a/tex/beautysource.png b/tex/beautysource.png
new file mode 100644
index 0000000000000000000000000000000000000000..984026628e3e3593d9804ef65c2ecd7c780d0376
Binary files /dev/null and b/tex/beautysource.png differ
diff --git a/tex/intro.tex b/tex/intro.tex
index a926dfb458e4a0b7a52deafa079e1096049f92ff..6309552dedf4abe3d5ba464dad8dd7cdced3f47b 100644
--- a/tex/intro.tex
+++ b/tex/intro.tex
@@ -19,13 +19,7 @@ To see what is known about beautiful sets, she types these three conditions into
 classifier, which interprets them as a \MMT theory $Q$, computes all (total) views from
 $Q$ into a library $\cL$, and returns presentations of target theories and the assignments
 made by the views. In our example we have the situation in
-Figure~\ref{fig:theory-classification-ex}\ednote{MK: Maybe better do this in jEdit and use
-  screenshots} \ednote{Interesting: the $\emptyset$ clause could also be ``$\exists S$
-  beautiful'', which is equivalent via the subset clause, maybe use that in the example:
-  define Matroid with that and have a theorem that says that $\emptyset$ is beautiful. Just
-  see what the viewfinder catches.\\
-  DM: It's not going to be a ``proper'' theorem because it will be difficult to construct a proof.
-  Apart from that it should still match Base, beautiful and the other axioms.}  In the base use case, Jane learns that her
+Figure~\ref{fig:theory-classification-ex}. In the base use case, Jane learns that her
 ``beautiful sets'' correspond to the well-known structure of
 matroids~\cite{wikipedia:matroid}, so she can directly apply matroid theory to her
 problems.
diff --git a/tex/matroids.png b/tex/matroids.png
new file mode 100644
index 0000000000000000000000000000000000000000..eb2eb882f91dd2510b4d23eb97ebcb20d448a286
Binary files /dev/null and b/tex/matroids.png differ
diff --git a/tex/results.png b/tex/results.png
new file mode 100644
index 0000000000000000000000000000000000000000..bcc9b82f4c020852d073d4c88ef195b508edb03f
Binary files /dev/null and b/tex/results.png differ
diff --git a/tex/usecase.tex b/tex/usecase.tex
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..982088edc2355742f07f3058764210e17bbf9ce9 100644
--- a/tex/usecase.tex
+++ b/tex/usecase.tex
@@ -0,0 +1,24 @@
+The Viewfinder algorithm is implemented in the MMT system and exposed within the jEdit-IDE, allowing us to realize the use case
+stated in the introduction. A screenshot of Jane's theory of beautiful sets is given in Figure \ref{fig:use:source}; it
+is based on the (basic higher-order logic) foundation of the Math-in-the-Middle\ednote{cite} library developed natively in MMT.
+
+\begin{figure}[ht]\centering
+  \fbox{\includegraphics[width=0.6\textwidth]{beautysource}}
+  \fbox{\includegraphics[width=\textwidth]{results}}
+\caption{A Theory of ``Beautiful Sets'' in MMT Surface Syntax and Results of the Viewfinder}\label{fig:use:source}
+\end{figure}
+
+Right-clicking anywhere within the theory allows Jane to select \cn{MMT} $\to$ \cn{Find\ Views\ to...} $\to$ \cn{MitM/smglom} (the main Math-in-the-Middle library), telling her (within less than one second) that 11 Views have been found, the most promising of which points to the theory
+\cn{matroid\_theory} (see Figure \ref{fig:use:target}) in the library.
+
+\begin{figure}[ht]\centering
+  \fbox{\includegraphics[width=0.6\textwidth]{matroids}}
+\caption{The Theory of Matroids in the MitM Library}\label{fig:use:target}
+\end{figure}
+
+\paragraph{} Using a different library as target, we can for example quickly write down a theory for a commutative binary operator (still using the Math-in-the-Middle foundation), allowing us to search e.g. the PVS Prelude library for any commutative operators, as in Figure \ref{fig:use:pvs}.
+
+\begin{figure}
+Hier könnte Ihre Werbung stehen
+\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
+\end{figure}
\ No newline at end of file