Simple Example 
from
Set Theory

Suppose we want to prove

if A⊆B: A∖C=A⋂(B∖C)

In a first step, we need to introduce the set theoretic notions via definitions. (Once the set theory prover is ported from Theorema 1.0 to the new version, the definitions can be dropped since the prover will then recognize all set theory constructs …)