[#] ( 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

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