let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0
for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
let A be OSSubset of OU0; :: thesis: for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
let s be SortSymbol of S1; :: thesis: the Sorts of OU0 . s in OSSubSort (A,s)
( the Sorts of OU0 is ManySortedSubset of the Sorts of OU0 & the Sorts of OU0 is OrderSortedSet of S1 ) by OSALG_1:17, PBOOLE:def 18;
then reconsider B = the Sorts of OU0 as OSSubset of OU0 by Def2;
the Sorts of OU0 in OSSubSort A by Th17;
then B . s in OSSubSort (A,s) by Def10;
hence the Sorts of OU0 . s in OSSubSort (A,s) ; :: thesis: verum