let S1 be OrderSortedSign; for U1 being monotone OSAlgebra of S1
for U2 being OSSubAlgebra of U1 holds U2 is monotone
let U1 be monotone OSAlgebra of S1; for U2 being OSSubAlgebra of U1 holds U2 is monotone
let U2 be OSSubAlgebra of U1; U2 is monotone
let o1, o2 be OperSymbol of S1; OSALG_1:def 21 ( not o1 <= o2 or (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) )
assume A1:
o1 <= o2
; (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)
; verum