set a = MSSubSort A;
reconsider u1 = U0 | (MSSubSort A) as strict MSSubAlgebra of U0 ;
take u1 ; :: thesis: ( A is MSSubset of u1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1 ) )
A1: u1 = MSAlgebra(# (MSSubSort A),(Opers (U0,(MSSubSort A))) #) by Def15, Th20;
A c= MSSubSort A by Th20;
hence A is MSSubset of u1 by A1, PBOOLE:def 18; :: thesis: for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1
let U2 be MSSubAlgebra of U0; :: thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 )
reconsider B = the Sorts of U2 as MSSubset of U0 by Def9;
assume A is MSSubset of U2 ; :: thesis: u1 is MSSubAlgebra of U2
then A2: A c= B by PBOOLE:def 18;
Constants U0 is MSSubset of U2 by Th10;
then A3: Constants U0 c= B by PBOOLE:def 18;
B is opers_closed by Def9;
then A4: B in SubSort A by A2, A3, Th13;
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 S or the Sorts of u1 . i c= the Sorts of U2 . i )
assume i in the carrier of S ; :: thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S ;
( the Sorts of u1 . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A1, A4, Def13, Def14;
hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; :: thesis: verum

end;

hence u1 is MSSubAlgebra of U2 by Th8; :: thesis: verum