let S be non empty non void ManySortedSign ; for MA being strict non-empty MSAlgebra over S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let MA be strict non-empty MSAlgebra over S; for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let F be SubsetFamily of the Sorts of MA; ( F c= SubSort MA implies for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed )
assume A1:
F c= SubSort MA
; for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let B be MSSubset of MA; ( B = meet |:F:| implies B is opers_closed )
assume A2:
B = meet |:F:|
; B is opers_closed
per cases
( F = {} or F <> {} )
;
suppose A8:
F <> {}
;
B is opers_closed set SS =
S;
let o be
OperSymbol of
S;
MSUALG_2:def 6 B is_closed_on oset i =
the_result_sort_of o;
A9:
the
ResultSort of
S . o = the_result_sort_of o
by MSUALG_1:def 2;
A10:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
( the
Arity of
S . o = the_arity_of o &
dom the
Arity of
S = the
carrier' of
S )
by FUNCT_2:def 1, MSUALG_1:def 1;
then A11:
((B #) * the Arity of S) . o = (B #) . (the_arity_of o)
by FUNCT_1:13;
Result (
o,
MA) =
( the Sorts of MA * the ResultSort of S) . o
by MSUALG_1:def 5
.=
the
Sorts of
MA . (the_result_sort_of o)
by A9, A10, FUNCT_1:13
;
then A12:
rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= the
Sorts of
MA . (the_result_sort_of o)
by RELAT_1:def 19;
A13:
rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= B . (the_result_sort_of o)
proof
consider Q being
Subset-Family of
( the Sorts of MA . (the_result_sort_of o)) such that A14:
Q = |:F:| . (the_result_sort_of o)
and A15:
B . (the_result_sort_of o) = Intersect Q
by A2, MSSUBFAM:def 1;
let v be
object ;
TARSKI:def 3 ( not v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) or v in B . (the_result_sort_of o) )
assume A16:
v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o)))
;
v in B . (the_result_sort_of o)
then consider p being
object such that A17:
p in dom ((Den (o,MA)) | ((B #) . (the_arity_of o)))
and A18:
v = ((Den (o,MA)) | ((B #) . (the_arity_of o))) . p
by FUNCT_1:def 3;
for
Y being
set st
Y in Q holds
v in Y
proof
A19:
|:F:| . (the_result_sort_of o) = { (xx . (the_result_sort_of o)) where xx is Element of Bool the Sorts of MA : xx in F }
by A8, CLOSURE2:14;
let Y be
set ;
( Y in Q implies v in Y )
assume
Y in Q
;
v in Y
then consider xx being
Element of
Bool the
Sorts of
MA such that A20:
Y = xx . (the_result_sort_of o)
and A21:
xx in F
by A14, A19;
reconsider xx =
xx as
MSSubset of
MA ;
xx is
opers_closed
by A1, A21, MSUALG_2:14;
then
xx is_closed_on o
;
then A22:
rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) c= (xx * the ResultSort of S) . o
;
B c= xx
by A2, A21, CLOSURE2:21, MSSUBFAM:43;
then
(Den (o,MA)) | (((B #) * the Arity of S) . o) c= (Den (o,MA)) | (((xx #) * the Arity of S) . o)
by MSUALG_2:2, RELAT_1:75;
then A23:
dom ((Den (o,MA)) | (((B #) * the Arity of S) . o)) c= dom ((Den (o,MA)) | (((xx #) * the Arity of S) . o))
by RELAT_1:11;
A24:
v = (Den (o,MA)) . p
by A17, A18, FUNCT_1:47;
then
v = ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) . p
by A11, A17, A23, FUNCT_1:47;
then
v in rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o))
by A11, A17, A23, FUNCT_1:def 3;
then
(Den (o,MA)) . p in (xx * the ResultSort of S) . o
by A22, A24;
then
(Den (o,MA)) . p in xx . ( the ResultSort of S . o)
by A10, FUNCT_1:13;
then
(Den (o,MA)) . p in xx . (the_result_sort_of o)
by MSUALG_1:def 2;
hence
v in Y
by A17, A18, A20, FUNCT_1:47;
verum
end;
hence
v in B . (the_result_sort_of o)
by A12, A16, A15, SETFAM_1:43;
verum
end;
(B * the ResultSort of S) . o = B . (the_result_sort_of o)
by A9, A10, FUNCT_1:13;
hence
B is_closed_on o
by A11, A13;
verum end;