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

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