set O = OwnSymbolsOf S;
set f = I | (OwnSymbolsOf S);
set D = dom (I | (OwnSymbolsOf S));
set C = U \/ BOOLEAN;
( OwnSymbolsOf S c= dom (I | (OwnSymbolsOf S)) & dom (I | (OwnSymbolsOf S)) c= OwnSymbolsOf S ) by Lm18, RELAT_1:def 18;
then dom (I | (OwnSymbolsOf S)) = OwnSymbolsOf S by XBOOLE_0:def 10;
hence for b₁ being OwnSymbolsOf S -defined Relation st b₁ = I | (OwnSymbolsOf S) holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum