let S1 be OrderSortedSign; :: thesis: for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic
let U1 be OSAlgebra of S1; :: thesis: U1,U1 are_os_isomorphic
take id the Sorts of U1 ; :: according to OSALG_3:def 2 :: thesis: ( id the Sorts of U1 is_isomorphism U1,U1 & id the Sorts of U1 is order-sorted )
the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17;
hence ( id the Sorts of U1 is_isomorphism U1,U1 & id the Sorts of U1 is order-sorted ) by MSUALG_3:16; :: thesis: verum