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 ) )
A1: B is OrderSortedSet of by Def2;
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 consider B1 being Element of SubSort A such that
A2: ( B1 = B & B1 is OrderSortedSet of ) ;
( B is opers_closed & Constants OU0 c= B & A c= B ) by A2, MSUALG_2:14;
hence ( B is opers_closed & OSConstants OU0 c= B & A c= B ) by Th16; :: thesis: verum

end;

assume A3: ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ; :: thesis: B in OSSubSort A
Constants OU0 c= OSConstants OU0 by Th15;
then Constants OU0 c= B by A3, PBOOLE:15;
then B in SubSort A by A3, MSUALG_2:14;
hence B in OSSubSort A by A1; :: thesis: verum