let S1 be OrderSortedSign; :: thesis: for U1 being monotone OSAlgebra of S1

for U2 being OSSubAlgebra of U1 holds U2 is monotone

let U1 be monotone OSAlgebra of S1; :: thesis: for U2 being OSSubAlgebra of U1 holds U2 is monotone

let U2 be OSSubAlgebra of U1; :: thesis: U2 is monotone

let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def 21 :: thesis: ( not o1 <= o2 or (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) )

assume A1: o1 <= o2 ; :: thesis: (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2)

A2: Args (o1,U2) c= Args (o2,U2) by A1, OSALG_1:26;

( the Sorts of U2 is MSSubset of U1 & the Sorts of U2 is OrderSortedSet of S1 ) by MSUALG_2:def 9, OSALG_1:17;

then reconsider B = the Sorts of U2 as OSSubset of U1 by OSALG_2:def 2;

A3: B is opers_closed by MSUALG_2:def 9;

then A4: B is_closed_on o1 by MSUALG_2:def 6;

A5: B is_closed_on o2 by A3, MSUALG_2:def 6;

A6: Den (o2,U2) = the Charact of U2 . o2 by MSUALG_1:def 6

.= (Opers (U1,B)) . o2 by MSUALG_2:def 9

.= o2 /. B by MSUALG_2:def 8

.= (Den (o2,U1)) | (((B #) * the Arity of S1) . o2) by A5, MSUALG_2:def 7

.= (Den (o2,U1)) | (Args (o2,U2)) by MSUALG_1:def 4 ;

A7: Den (o1,U2) = the Charact of U2 . o1 by MSUALG_1:def 6

.= (Opers (U1,B)) . o1 by MSUALG_2:def 9

.= o1 /. B by MSUALG_2:def 8

.= (Den (o1,U1)) | (((B #) * the Arity of S1) . o1) by A4, MSUALG_2:def 7

.= (Den (o1,U1)) | (Args (o1,U2)) by MSUALG_1:def 4 ;

(Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) by A1, OSALG_1:def 21;

then Den (o1,U2) = (Den (o2,U1)) | ((Args (o1,U1)) /\ (Args (o1,U2))) by A7, RELAT_1:71

.= (Den (o2,U1)) | (Args (o1,U2)) by MSAFREE3:37, XBOOLE_1:28

.= (Den (o2,U1)) | ((Args (o2,U2)) /\ (Args (o1,U2))) by A2, XBOOLE_1:28

.= (Den (o2,U2)) | (Args (o1,U2)) by A6, RELAT_1:71 ;

hence (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) ; :: thesis: verum

for U2 being OSSubAlgebra of U1 holds U2 is monotone

let U1 be monotone OSAlgebra of S1; :: thesis: for U2 being OSSubAlgebra of U1 holds U2 is monotone

let U2 be OSSubAlgebra of U1; :: thesis: U2 is monotone

let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def 21 :: thesis: ( not o1 <= o2 or (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) )

assume A1: o1 <= o2 ; :: thesis: (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2)

A2: Args (o1,U2) c= Args (o2,U2) by A1, OSALG_1:26;

( the Sorts of U2 is MSSubset of U1 & the Sorts of U2 is OrderSortedSet of S1 ) by MSUALG_2:def 9, OSALG_1:17;

then reconsider B = the Sorts of U2 as OSSubset of U1 by OSALG_2:def 2;

A3: B is opers_closed by MSUALG_2:def 9;

then A4: B is_closed_on o1 by MSUALG_2:def 6;

A5: B is_closed_on o2 by A3, MSUALG_2:def 6;

A6: Den (o2,U2) = the Charact of U2 . o2 by MSUALG_1:def 6

.= (Opers (U1,B)) . o2 by MSUALG_2:def 9

.= o2 /. B by MSUALG_2:def 8

.= (Den (o2,U1)) | (((B #) * the Arity of S1) . o2) by A5, MSUALG_2:def 7

.= (Den (o2,U1)) | (Args (o2,U2)) by MSUALG_1:def 4 ;

A7: Den (o1,U2) = the Charact of U2 . o1 by MSUALG_1:def 6

.= (Opers (U1,B)) . o1 by MSUALG_2:def 9

.= o1 /. B by MSUALG_2:def 8

.= (Den (o1,U1)) | (((B #) * the Arity of S1) . o1) by A4, MSUALG_2:def 7

.= (Den (o1,U1)) | (Args (o1,U2)) by MSUALG_1:def 4 ;

(Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) by A1, OSALG_1:def 21;

then Den (o1,U2) = (Den (o2,U1)) | ((Args (o1,U1)) /\ (Args (o1,U2))) by A7, RELAT_1:71

.= (Den (o2,U1)) | (Args (o1,U2)) by MSAFREE3:37, XBOOLE_1:28

.= (Den (o2,U1)) | ((Args (o2,U2)) /\ (Args (o1,U2))) by A2, XBOOLE_1:28

.= (Den (o2,U2)) | (Args (o1,U2)) by A6, RELAT_1:71 ;

hence (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) ; :: thesis: verum