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