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

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