reconsider Y = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
set X = the OrderSortedRelation of Y;
reconsider X1 = the OrderSortedRelation of Y as ManySortedRelation of U1 ;
take X1 ; :: thesis: X1 is os-compatible
thus X1 is os-compatible ; :: thesis: verum