(Constants U0) \/ A is non-empty ;
then reconsider a = MSSubSort A as V8() MSSubset of U0 by Th17;
A1: ( a is opers_closed & A c= a ) by Th21;
then U0 | a = MSAlgebra(# a,(Opers U0,a) #) by Def16;
then reconsider u1 = U0 | a as strict non-empty MSSubAlgebra of U0 by MSUALG_1:def 8;

now

A2: u1 = MSAlgebra(# a,(Opers U0,a) #) by A1, Def16;
hence A is MSSubset of u1 by A1, PBOOLE:def 23; :: thesis: for U2 being MSSubAlgebra of U0 st A is MSSubset of U2 holds
u1 is MSSubAlgebra of U2
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 Def10;
A3: B is opers_closed by Def10;
assume A is MSSubset of U2 ; :: thesis: u1 is MSSubAlgebra of U2
then A4: A c= B by PBOOLE:def 23;
Constants U0 is MSSubset of U2 by Th11;
then Constants U0 c= B by PBOOLE:def 23;
then A5: B in SubSort A by A3, A4, Th14;
the Sorts of u1 c= the Sorts of U2

proof

let i be set ; :: according to PBOOLE:def 5 :: 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 ;
A6: the Sorts of u1 . s = meet (SubSort A,s) by A2, Def15;
B . s in SubSort A,s by A5, Def14;
hence the Sorts of u1 . i c= the Sorts of U2 . i by A6, SETFAM_1:4; :: thesis: verum

end;

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

end;

hence GenMSAlg A is non-empty by Def18; :: thesis: verum