let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A
let A be OSSubset of OU0; :: thesis: the Sorts of OU0 in OSSubSort A
reconsider X = the Sorts of OU0 as Element of SubSort A by MSUALG_2:40;
the Sorts of OU0 is OrderSortedSet of S1 by OSALG_1:17;
then X in { x where x is Element of SubSort A : x is OrderSortedSet of S1 } ;
hence the Sorts of OU0 in OSSubSort A ; :: thesis: verum