OwnSymbolsOf S c= dom I by Lm2;
hence for b₁ being set st b₁ = (OwnSymbolsOf S) \ (dom I) holds
b₁ is empty ; :: thesis: verum