set x = the Element of OSSubSort OU0;
the Element of OSSubSort OU0 in { y where y is Element of SubSort OU0 : y is OrderSortedSet of S1 } ;
then consider x1 being Element of SubSort OU0 such that
the Element of OSSubSort OU0 = x1 and
A1: x1 is OrderSortedSet of S1 ;
reconsider x2 = x1 as MSSubset of OU0 by MSUALG_2:def 11;
reconsider x3 = x2 as OSSubset of OU0 by A1, Def2;
take x3 ; :: thesis: x3 is opers_closed
thus x3 is opers_closed by MSUALG_2:def 11; :: thesis: verum