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