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 & [#] ( the Sorts of L . the formula-sort of S) is with_equality )
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 & [#] ( the Sorts of L . the formula-sort of S) is with_equality ) ; :: thesis: verum