set S1 = S;
set SS1 = AllSymbolsOf S;
set SX = SymbolsOf X;
set add = ((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet ;
set f = (((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0;
set S2 = S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0);
set SS2 = AllSymbolsOf (S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0));
(AllSymbolsOf (S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0))) \+\ ((dom ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0)) \/ (AllSymbolsOf S)) = {} ;
then AllSymbolsOf (S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0)) = (dom ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0)) \/ (AllSymbolsOf S) by FOMODEL0:29
.= (((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) \/ (AllSymbolsOf S) ;
hence for b₁ being 1-sorted st b₁ = S addLettersNotIn X holds
b₁ is countable by ORDERS_4:def 2; :: thesis: verum