set E = Subformulae F;
Subformulae F is Subset of by SUBSET:3;
hence Subformulae F is Subset of by MODELC_2:47; :: thesis: verum