let S be OrderSortedSign; :: thesis: for U0 being OSAlgebra of S
for U1 being MSAlgebra of S holds
( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U0,B ) ) ) )
let U0 be OSAlgebra of S; :: thesis: for U1 being MSAlgebra of S holds
( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U0,B ) ) ) )
let U1 be MSAlgebra of S; :: thesis: ( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U0,B ) ) ) )

hereby :: thesis: ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U0,B ) ) implies U1 is OSSubAlgebra of U0 )

assume A1: U1 is OSSubAlgebra of U0 ; :: thesis: ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U0,B ) ) )
then A2: the Sorts of U1 is OrderSortedSet of by OSALG_1:17;
the Sorts of U1 is MSSubset of U0 by A1, MSUALG_2:def 10;
hence the Sorts of U1 is OSSubset of U0 by A2, Def2; :: thesis: for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U0,B )
let B be OSSubset of U0; :: thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers U0,B ) )
assume A3: B = the Sorts of U1 ; :: thesis: ( B is opers_closed & the Charact of U1 = Opers U0,B )
thus ( B is opers_closed & the Charact of U1 = Opers U0,B ) by A1, A3, MSUALG_2:def 10; :: thesis: verum

end;

assume A4: the Sorts of U1 is OSSubset of U0 ; :: thesis: ( ex B being OSSubset of U0 st
( B = the Sorts of U1 & not ( B is opers_closed & the Charact of U1 = Opers U0,B ) ) or U1 is OSSubAlgebra of U0 )
then A5: the Sorts of U1 is OrderSortedSet of by Def2;
assume A6: for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U0,B ) ; :: thesis: U1 is OSSubAlgebra of U0
U1 is MSSubAlgebra of U0

proof

thus the Sorts of U1 is MSSubset of U0 by A4; :: according to MSUALG_2:def 10 :: thesis: for b₁ being ManySortedSubset of the Sorts of U0 holds
( not b₁ = the Sorts of U1 or ( b₁ is opers_closed & the Charact of U1 = Opers U0,b₁ ) )
let B be MSSubset of U0; :: thesis: ( not B = the Sorts of U1 or ( B is opers_closed & the Charact of U1 = Opers U0,B ) )
assume A7: B = the Sorts of U1 ; :: thesis: ( B is opers_closed & the Charact of U1 = Opers U0,B )
reconsider B1 = B as OSSubset of U0 by A4, A7;
( B1 is opers_closed & the Charact of U1 = Opers U0,B1 ) by A6, A7;
hence ( B is opers_closed & the Charact of U1 = Opers U0,B ) ; :: thesis: verum

end;

hence U1 is OSSubAlgebra of U0 by A5, OSALG_1:17; :: thesis: verum