let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for B being OSSubset of OU0 holds
( B in OSSubSort OU0 iff B is opers_closed )
let OU0 be OSAlgebra of S1; :: thesis: for B being OSSubset of OU0 holds
( B in OSSubSort OU0 iff B is opers_closed )
let B be OSSubset of OU0; :: thesis: ( B in OSSubSort OU0 iff B is opers_closed )
A1: ( B in SubSort OU0 iff B is opers_closed ) by MSUALG_2:14;
thus ( B in OSSubSort OU0 implies B is opers_closed ) :: thesis: ( B is opers_closed implies B in OSSubSort OU0 )

proof

assume B in OSSubSort OU0 ; :: thesis: B is opers_closed
then ex B1 being Element of SubSort OU0 st
( B1 = B & B1 is OrderSortedSet of S1 ) ;
hence B is opers_closed by MSUALG_2:14; :: thesis: verum

end;

assume A2: B is opers_closed ; :: thesis: B in OSSubSort OU0
B is OrderSortedSet of S1 by Def2;
hence B in OSSubSort OU0 by A1, A2; :: thesis: verum