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

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