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

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