let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds
( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
let A be OSSubset of OU0; :: thesis: ( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
set a = OSMSubSort A;
reconsider u1 = OU0 | (OSMSubSort A) as strict OSSubAlgebra of OU0 ;
A1: u1 = MSAlgebra(# (OSMSubSort A),(Opers (OU0,(OSMSubSort A))) #) by MSUALG_2:def 15;
A2: A c= OSMSubSort A by Th29;
A3: A is OrderSortedSet of S1 by Def2;
A4: ( A is OSSubset of u1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1 ) )

proof

A is MSSubset of u1 by A2, A1, PBOOLE:def 18;
hence A is OSSubset of u1 by A3, Def2; :: thesis: for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1
let U2 be OSSubAlgebra of OU0; :: thesis: ( A is OSSubset of U2 implies u1 is OSSubAlgebra of U2 )
reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def 9;
B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
assume A is OSSubset of U2 ; :: thesis: u1 is OSSubAlgebra of U2
then A5: ( B is opers_closed & A c= B ) by MSUALG_2:def 9, PBOOLE:def 18;
OSConstants OU0 is OSSubset of U2 by Th13;
then OSConstants OU0 c= B by PBOOLE:def 18;
then A6: B in OSSubSort A by A5, Th19;
the Sorts of u1 c= the Sorts of U2

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S1 or the Sorts of u1 . i c= the Sorts of U2 . i )
assume i in the carrier of S1 ; :: thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S1 ;
( the Sorts of u1 . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, A6, Def10, Def11;
hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; :: thesis: verum

end;

hence u1 is OSSubAlgebra of U2 by MSUALG_2:8; :: thesis: verum

end;

hence GenOSAlg A = OU0 | (OSMSubSort A) by Def12; :: thesis: the Sorts of (GenOSAlg A) = OSMSubSort A
thus the Sorts of (GenOSAlg A) = OSMSubSort A by A1, A4, Def12; :: thesis: verum