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