let S be OrderSortedSign; :: thesis: for U0 being OSAlgebra of S
for U1 being MSAlgebra over 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 over 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 over 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 ( the Sorts of U1 is OrderSortedSet of S & the Sorts of U1 is MSSubset of U0 ) by MSUALG_2:def 9, OSALG_1:17;
hence the Sorts of U1 is OSSubset of U0 by 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 B = the Sorts of U1 ; :: thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) )
hence ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) by A1, MSUALG_2:def 9; :: thesis: verum

end;

assume A2: 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 )
assume A3: 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
A4: U1 is MSSubAlgebra of U0

proof

thus the Sorts of U1 is MSSubset of U0 by A2; :: according to MSUALG_2:def 9 :: 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 A5: 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 A2, A5;
B1 is opers_closed by A3, A5;
hence ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) by A3, A5; :: thesis: verum

end;

the Sorts of U1 is OrderSortedSet of S by A2, Def2;
hence U1 is OSSubAlgebra of U0 by A4, OSALG_1:17; :: thesis: verum