set f = (D,num) AddFormulasTo X;
set XX = (D,num) CompletionOf X;
reconsider ff = (D,num) AddFormulasTo X as Function of NAT,(rng ((D,num) AddFormulasTo X)) by FUNCT_2:6;
ff . 0 in rng ((D,num) AddFormulasTo X) ;
then ((D,num) AddFormulasTo X) . 0 c= (D,num) CompletionOf X by ZFMISC_1:74;
then X c= (D,num) CompletionOf X by DefAdd2;
hence for b₁ being set st b₁ = X \ ((D,num) CompletionOf X) holds
b₁ is empty ; :: thesis: verum