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 is OrderSortedSet of by Def2;
A2: ( B in SubSort OU0 iff B is opers_closed ) by MSUALG_2:15;
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 consider B1 being Element of SubSort OU0 such that
A3: ( B1 = B & B1 is OrderSortedSet of ) ;
thus B is opers_closed by A3, MSUALG_2:15; :: thesis: verum

end;

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