consider x being Element of OSSubSort OU0;
x in { y where y is Element of SubSort OU0 : y is OrderSortedSet of S1 } ;
then consider x1 being Element of SubSort OU0 such that
x = x1 and
A1: x1 is OrderSortedSet of S1 ;
reconsider x2 = x1 as MSSubset of OU0 by MSUALG_2:def 12;
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 12; :: thesis: verum