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

( 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