set SUI = U -InterpretersOf S;
set O = OwnSymbolsOf S;
set C = PFuncs ((U *),(U \/ BOOLEAN));
let x be Element of U -InterpretersOf S; :: thesis: x is S,U -interpreter-like
x in U -InterpretersOf S ;
then consider f being Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) such that
A1: ( x = f & f is S,U -interpreter-like ) ;
thus x is S,U -interpreter-like by A1; :: thesis: verum