set a = OSMSubSort A;
reconsider u1 = OU0 | (OSMSubSort A) as strict OSSubAlgebra of OU0 ;
take u1 ; :: thesis: ( A is OSSubset of u1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1 ) )
A1: u1 = MSAlgebra(# (OSMSubSort A),(Opers (OU0,(OSMSubSort A))) #) by MSUALG_2:def 15;
A2: A is OrderSortedSet of S1 by Def2;
A c= OSMSubSort A by Th29;
then A is MSSubset of u1 by A1, PBOOLE:def 18;
hence A is OSSubset of u1 by A2, 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 A3: ( 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 A4: B in OSSubSort A by A3, 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, A4, 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