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)

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

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

then
bool (union (rng B)) c= bool (union (rng the Sorts of U0))
by ZFMISC_1:67;
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;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

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