let S1 be OrderSortedSign; :: thesis: for U1, U2 being strict non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds
( U1 is monotone iff U2 is monotone )
let U1, U2 be strict non-empty OSAlgebra of S1; :: thesis: ( U1,U2 are_os_isomorphic implies ( U1 is monotone iff U2 is monotone ) )
assume U1,U2 are_os_isomorphic ; :: thesis: ( U1 is monotone iff U2 is monotone )
then consider F being ManySortedFunction of U1,U2 such that
A1: F is_isomorphism U1,U2 and
A2: F is order-sorted ;
reconsider O1 = the Sorts of U1, O2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17;
reconsider F1 = F as ManySortedFunction of O1,O2 ;
( F is "onto" & F is "1-1" ) by A1, MSUALG_3:13;
then A3: F1 "" is order-sorted by A2, Th6;
A4: F is_epimorphism U1,U2 by A1, MSUALG_3:def 10;
then A5: F is_homomorphism U1,U2 by MSUALG_3:def 8;
then Image F = U2 by A4, MSUALG_3:19;
hence ( U1 is monotone implies U2 is monotone ) by A2, A5, Th13; :: thesis: ( U2 is monotone implies U1 is monotone )
reconsider F2 = F1 "" as ManySortedFunction of U2,U1 ;
assume A6: U2 is monotone ; :: thesis: U1 is monotone
F "" is_isomorphism U2,U1 by A1, MSUALG_3:14;
then A7: F2 is_epimorphism U2,U1 by MSUALG_3:def 10;
then A8: F2 is_homomorphism U2,U1 by MSUALG_3:def 8;
then Image F2 = U1 by A7, MSUALG_3:19;
hence U1 is monotone by A3, A8, A6, Th13; :: thesis: verum