set AF = AllFormulasOf S;
reconsider AFF = AllFormulasOf S as Subset of (AllFormulasOf S) by XBOOLE_0:def 10;
take AFF ; :: thesis: AFF is D -expanded
thus AFF is D -expanded by Lm26; :: thesis: verum