set M = MSAlgebra(# A,(Opers (OU0,A)) #);
( OU0 | A = MSAlgebra(# A,(Opers (OU0,A)) #) & A is OrderSortedSet of S1 ) by Def2, MSUALG_2:def 15;
hence OU0 | A is order-sorted by OSALG_1:17; :: thesis: verum