[#] ( the Sorts of L . the formula-sort of S) = the Sorts of L . the formula-sort of S by SUBSET_1:def 3;
hence [#] ( the Sorts of L . the formula-sort of S) is with_equality ; :: thesis: verum