set FF = AllFormulasOf S;
set Y = X \/ (AllFormulasOf S);
set f = (D,num) AddFormulasTo X;
reconsider F = rng ((D,num) AddFormulasTo X) as Subset of (bool (X \/ (AllFormulasOf S))) by RELAT_1:def 19;
(union F) \ (X \/ (AllFormulasOf S)) = {} ;
hence union (rng ((D,num) AddFormulasTo X)) is Subset of (X \/ (AllFormulasOf S)) ; :: thesis: verum