set II = I quotient E;
set O = OwnSymbolsOf S;
dom (I quotient E) c= OwnSymbolsOf S by Def17;
hence I quotient E is OwnSymbolsOf S -defined by RELAT_1:def 18; :: thesis: verum