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