let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A, B being OSSubset of OU0 holds
( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
let OU0 be OSAlgebra of S1; :: thesis: for A, B being OSSubset of OU0 holds
( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
let A, B be OSSubset of OU0; :: thesis: ( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
thus ( B in OSSubSort A implies ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ) :: thesis: ( B is opers_closed & OSConstants OU0 c= B & A c= B implies B in OSSubSort A )

proof

assume B in OSSubSort A ; :: thesis: ( B is opers_closed & OSConstants OU0 c= B & A c= B )
then A1: ex B1 being Element of SubSort A st
( B1 = B & B1 is OrderSortedSet of S1 ) ;
then Constants OU0 c= B by MSUALG_2:13;
hence ( B is opers_closed & OSConstants OU0 c= B & A c= B ) by A1, Th11, MSUALG_2:13; :: thesis: verum

end;

assume that
A2: B is opers_closed and
A3: OSConstants OU0 c= B and
A4: A c= B ; :: thesis: B in OSSubSort A
Constants OU0 c= OSConstants OU0 by Th10;
then Constants OU0 c= B by A3, PBOOLE:13;
then A5: B in SubSort A by A2, A4, MSUALG_2:13;
B is OrderSortedSet of S1 by Def2;
hence B in OSSubSort A by A5; :: thesis: verum