let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for B being MSSubset of U0 holds
( B in SubSort U0 iff B is opers_closed )
let U0 be MSAlgebra over S; :: thesis: for B being MSSubset of U0 holds
( B in SubSort U0 iff B is opers_closed )
let B be MSSubset of U0; :: thesis: ( B in SubSort U0 iff B is opers_closed )
set C = bool (Union the Sorts of U0);
A1: dom B = the carrier of S by PARTFUN1:def 2;
A2: dom the Sorts of U0 = the carrier of S by PARTFUN1:def 2;
union (rng B) c= union (rng the Sorts of U0)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng B) or x in union (rng the Sorts of U0) )
assume x in union (rng B) ; :: thesis: x in union (rng the Sorts of U0)
then consider Y being set such that
A3: x in Y and
A4: Y in rng B by TARSKI:def 4;
consider y being object such that
A5: y in dom B and
A6: B . y = Y by A4, FUNCT_1:def 3;
A7: the Sorts of U0 . y in rng the Sorts of U0 by A1, A2, A5, FUNCT_1:def 3;
B c= the Sorts of U0 by PBOOLE:def 18;
then B . y c= the Sorts of U0 . y by A1, A5;
hence x in union (rng the Sorts of U0) by A3, A6, A7, TARSKI:def 4; :: thesis: verum
end;
then bool (union (rng B)) c= bool (union (rng the Sorts of U0)) by ZFMISC_1:67;
then A8: bool (union (rng B)) c= bool (Union the Sorts of U0) by CARD_3:def 4;
thus ( B in SubSort U0 implies B is opers_closed ) by Def11; :: thesis: ( B is opers_closed implies B in SubSort U0 )
assume B is opers_closed ; :: thesis: B in SubSort U0
then A9: for C being MSSubset of U0 st C = B holds
C is opers_closed ;
rng B c= bool (union (rng B)) by ZFMISC_1:82;
then rng B c= bool (Union the Sorts of U0) by A8;
then B in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by A1, FUNCT_2:def 2;
hence B in SubSort U0 by A9, Def11; :: thesis: verum