take [#] ( the Sorts of L . the formula-sort of S) ; :: thesis: ( [#] ( the Sorts of L . the formula-sort of S) is QC-closed & [#] ( the Sorts of L . the formula-sort of S) is PC-closed )
thus ( [#] ( the Sorts of L . the formula-sort of S) is QC-closed & [#] ( the Sorts of L . the formula-sort of S) is PC-closed ) ; :: thesis: verum