set II = U -InterpretersOf S;
take the Element of U -InterpretersOf S ; :: thesis: the Element of U -InterpretersOf S is OwnSymbolsOf S -defined
thus the Element of U -InterpretersOf S is OwnSymbolsOf S -defined ; :: thesis: verum