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 23 :: 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 10, 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 10;
then A4: B is_closed_on o1 by MSUALG_2:def 7;
A5: B is_closed_on o2 by A3, MSUALG_2:def 7;
A6: Den o2,U2 = the Charact of U2 . o2 by MSUALG_1:def 11
.= (Opers U1,B) . o2 by MSUALG_2:def 10
.= o2 /. B by MSUALG_2:def 9
.= (Den o2,U1) | (((B # ) * the Arity of S1) . o2) by A5, MSUALG_2:def 8
.= (Den o2,U1) | (Args o2,U2) by MSUALG_1:def 9 ;
A7: Den o1,U2 = the Charact of U2 . o1 by MSUALG_1:def 11
.= (Opers U1,B) . o1 by MSUALG_2:def 10
.= o1 /. B by MSUALG_2:def 9
.= (Den o1,U1) | (((B # ) * the Arity of S1) . o1) by A4, MSUALG_2:def 8
.= (Den o1,U1) | (Args o1,U2) by MSUALG_1:def 9 ;
(Den o2,U1) | (Args o1,U1) = Den o1,U1 by A1, OSALG_1:def 23;
then Den o1,U2 = (Den o2,U1) | ((Args o1,U1) /\ (Args o1,U2)) by A7, RELAT_1:100
.= (Den o2,U1) | (Args o1,U2) by MSAFREE3:38, 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:100 ;
hence (Den o2,U2) | (Args o1,U2) = Den o1,U2 ; :: thesis: verum