set J = I quotient E;
set O = OwnSymbolsOf S;
set II = (Class E) -InterpretersOf S;
(I quotient E) null (OwnSymbolsOf S) in (Class E) -InterpretersOf S by FOMODEL2:2;
hence I quotient E is Element of (Class E) -InterpretersOf S ; :: thesis: verum