set I = U -InterpretersOf S;
set O = OwnSymbolsOf S;
set C = PFuncs ((U *),(U \/ BOOLEAN));
defpred S₁[ Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN))))] means $1 is S,U -interpreter-like ;
{ f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : S₁[f] } is Subset of (Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN))))) from DOMAIN_1:sch 7();
hence U -InterpretersOf S is Subset of (Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN))))) ; :: thesis: verum