set EF = ExFormulasOf S;
set FF = AllFormulasOf S;
for x being object st x in ExFormulasOf S holds
x in AllFormulasOf S by Th16;
then ExFormulasOf S c= AllFormulasOf S ;
hence for b₁ being set st b₁ = (ExFormulasOf S) \ (AllFormulasOf S) holds
b₁ is empty ; :: thesis: verum