set AF = AllFormulasOf S;
take the D -expanded Subset of (AllFormulasOf S) ; :: thesis: the D -expanded Subset of (AllFormulasOf S) is D -expanded
thus the D -expanded Subset of (AllFormulasOf S) is D -expanded ; :: thesis: verum