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