(Constants U0) (\/) A is V8()
;

then reconsider a = MSSubSort A as V8() MSSubset of U0 by Th16;

U0 | a = MSAlgebra(# a,(Opers (U0,a)) #) by Def15, Th20;

then reconsider u1 = U0 | a as strict non-empty MSSubAlgebra of U0 by MSUALG_1:def 3;

A1: A c= a by Th20;

then reconsider a = MSSubSort A as V8() MSSubset of U0 by Th16;

U0 | a = MSAlgebra(# a,(Opers (U0,a)) #) by Def15, Th20;

then reconsider u1 = U0 | a as strict non-empty MSSubAlgebra of U0 by MSUALG_1:def 3;

A1: A c= a by Th20;

now :: thesis: ( A is MSSubset of u1 & ( for U2 being MSSubAlgebra of U0 st A is MSSubset of U2 holds

u1 is MSSubAlgebra of U2 ) )

hence
GenMSAlg A is non-empty
by Def17; :: thesis: verumu1 is MSSubAlgebra of U2 ) )

A2:
u1 = MSAlgebra(# a,(Opers (U0,a)) #)
by Def15, Th20;

hence A is MSSubset of u1 by A1, PBOOLE:def 18; :: 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 Def9;

assume A is MSSubset of U2 ; :: thesis: u1 is MSSubAlgebra of U2

then A3: A c= B by PBOOLE:def 18;

Constants U0 is MSSubset of U2 by Th10;

then A4: Constants U0 c= B by PBOOLE:def 18;

B is opers_closed by Def9;

then A5: B in SubSort A by A3, A4, Th13;

the Sorts of u1 c= the Sorts of U2

end;hence A is MSSubset of u1 by A1, PBOOLE:def 18; :: 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 Def9;

assume A is MSSubset of U2 ; :: thesis: u1 is MSSubAlgebra of U2

then A3: A c= B by PBOOLE:def 18;

Constants U0 is MSSubset of U2 by Th10;

then A4: Constants U0 c= B by PBOOLE:def 18;

B is opers_closed by Def9;

then A5: B in SubSort A by A3, A4, Th13;

the Sorts of u1 c= the Sorts of U2

proof

hence
u1 is MSSubAlgebra of U2
by Th8; :: thesis: verum
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 A2, A5, Def13, Def14;

hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; :: thesis: verum

end;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 A2, A5, Def13, Def14;

hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; :: thesis: verum