set A = the Sorts of U0;
reconsider A = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
A1:
A is OrderSortedSet of S
by OSALG_1:17;
then reconsider A = A as OSSubset of U0 by OSALG_2:def 2;
take
A
; for O being OSSubset of U0 st O = OSCl A holds
the Sorts of (GenOSAlg O) = the Sorts of U0
set G = GenOSAlg A;
A is OSSubset of GenOSAlg A
by OSALG_2:def 12;
then A2:
A c= the Sorts of (GenOSAlg A)
by PBOOLE:def 18;
the Sorts of (GenOSAlg A) is MSSubset of U0
by MSUALG_2:def 9;
then A3:
the Sorts of (GenOSAlg A) c= A
by PBOOLE:def 18;
A = OSCl A
by A1, OSALG_2:9;
hence
for O being OSSubset of U0 st O = OSCl A holds
the Sorts of (GenOSAlg O) = the Sorts of U0
by A2, A3, PBOOLE:146; verum