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

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