We prove:

under the assumptions:

In order to prove MouseOver we assume

and then prove

We expand definitions:

In order to prove MouseOver, using definition MouseOver, we now show

From MouseOver we know, by definition MouseOver,

For proving MouseOver we choose b arbitrary but fixed and assume

We have to show

For proving MouseOver we have to find an appropriate value for (SuperStar[a]), such that we can prove

We augment the knowledge base:

From MouseOver, using MouseOver, we can deduce

From MouseOver we know

for arbitrary but fixed a.

We apply substitutions:

In order to prove MouseOver, using MouseOver, we now show

We augment the knowledge base:

From MouseOver, using MouseOver, we can deduce

We expand definitions:

In order to prove MouseOver, using definition MouseOver, we now show

Let now (SuperStar[a])->u[a]. In order to prove MouseOver it suffices to show

The goal MouseOver is identical to formula MouseOver in the knowledge base. Thus, this part of the proof is finished.