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

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