set O = OwnSymbolsOf S;
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: I is OwnSymbolsOf S -defined
dom I c= OwnSymbolsOf S by Lm32;
hence I is OwnSymbolsOf S -defined by RELAT_1:def 18; :: thesis: verum