let S1 be OrderSortedSign; for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st Constants OU0 c= A holds
OSConstants OU0 c= A
let OU0 be OSAlgebra of S1; for A being OSSubset of OU0 st Constants OU0 c= A holds
OSConstants OU0 c= A
let A be OSSubset of OU0; ( Constants OU0 c= A implies OSConstants OU0 c= A )
assume A1:
Constants OU0 c= A
; OSConstants OU0 c= A
assume
not OSConstants OU0 c= A
; contradiction
then consider i being object such that
A2:
i in the carrier of S1
and
A3:
not (OSConstants OU0) . i c= A . i
;
reconsider s = i as SortSymbol of S1 by A2;
consider x being object such that
A4:
x in (OSConstants OU0) . i
and
A5:
not x in A . i
by A3;
(OSConstants OU0) . s =
OSConstants (OU0,s)
by Def5
.=
union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s }
;
then consider X1 being set such that
A6:
x in X1
and
A7:
X1 in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s }
by A4, TARSKI:def 4;
consider s1 being SortSymbol of S1 such that
A8:
X1 = Constants (OU0,s1)
and
A9:
s1 <= s
by A7;
A10:
(Constants OU0) . s1 c= A . s1
by A1;
x in (Constants OU0) . s1
by A6, A8, MSUALG_2:def 4;
then A11:
x in A . s1
by A10;
A is OrderSortedSet of S1
by Def2;
then
A . s1 c= A . s
by A9, OSALG_1:def 16;
hence
contradiction
by A5, A11; verum