:: MBOOLEAN semantic presentation

begin


definition
let I be set ;
let A be ManySortedSet of I;
func bool A ->  ManySortedSet of I means :Def1: :: MBOOLEAN:def 1
 for i being set st i in I holds
it . i = bool (A . i);
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = bool (A . i)
proof
deffunc H1( set ) ->  set = bool (A . $1);
thus  ex X being ManySortedSet of I st
for i being set st i in I holds
X . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = bool (A . i) ) & ( for i being set st i in I holds
b2 . i = bool (A . i) ) holds
b1 = b2
proof
let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
X . i = bool (A . i) ) & ( for i being set st i in I holds
Y . i = bool (A . i) ) implies X = Y )
assume that
A1: for i being set st i in I holds
X . i = bool (A . i) and
A2: for i being set st i in I holds
Y . i = bool (A . i) ; ::_thesis: X = Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_Y_._i
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume A3: i in I ; ::_thesis: X . i = Y . i
hence X . i = bool (A . i) by A1
.= Y . i by A2, A3 ;
::_thesis: verum
end;
hence  X = Y by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines bool MBOOLEAN:def_1_:_
 for I being set
for A, b3 being ManySortedSet of I holds
( b3 = bool A iff for i being set st i in I holds
b3 . i = bool (A . i) );

registration
let I be set ;
let A be ManySortedSet of I;
cluster bool A -> V2() ;
coherence
 bool A is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not (bool A) . i is empty )
assume A1: i in I ; ::_thesis: not (bool A) . i is empty
 not bool (A . i) is empty ;
hence  not (bool A) . i is empty by A1, Def1; ::_thesis: verum
end;
end;

Lm1:  for i, I, X being set
for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
proof
let i, I, X be set ; ::_thesis: for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
let M be ManySortedSet of I; ::_thesis: ( i in I implies dom (M +* (i .--> X)) = I )
assume A1: i in I ; ::_thesis: dom (M +* (i .--> X)) = I
thus  dom (M +* (i .--> X)) = (dom M) \/ (dom (i .--> X)) by FUNCT_4:def_1
.= I \/ (dom (i .--> X)) by PARTFUN1:def_2
.= I \/ {i} by FUNCOP_1:13
.= I by A1, ZFMISC_1:40 ; ::_thesis: verum
end;

Lm2:  for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
let i be set ; ::_thesis: ( i in I implies (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) )
assume A1: i in I ; ::_thesis: (bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
hence (bool (A \/ B)) . i = bool ((A \/ B) . i) by Def1
.= bool ((A . i) \/ (B . i)) by A1, PBOOLE:def_4 ;
::_thesis: verum
end;

Lm3:  for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
let i be set ; ::_thesis: ( i in I implies (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) )
assume A1: i in I ; ::_thesis: (bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
hence (bool (A /\ B)) . i = bool ((A /\ B) . i) by Def1
.= bool ((A . i) /\ (B . i)) by A1, PBOOLE:def_5 ;
::_thesis: verum
end;

Lm4:  for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \ B)) . i = bool ((A . i) \ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \ B)) . i = bool ((A . i) \ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(bool (A \ B)) . i = bool ((A . i) \ (B . i))
let i be set ; ::_thesis: ( i in I implies (bool (A \ B)) . i = bool ((A . i) \ (B . i)) )
assume A1: i in I ; ::_thesis: (bool (A \ B)) . i = bool ((A . i) \ (B . i))
hence (bool (A \ B)) . i = bool ((A \ B) . i) by Def1
.= bool ((A . i) \ (B . i)) by A1, PBOOLE:def_6 ;
::_thesis: verum
end;

Lm5:  for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
let i be set ; ::_thesis: ( i in I implies (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) )
assume A1: i in I ; ::_thesis: (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
hence (bool (A \+\ B)) . i = bool ((A \+\ B) . i) by Def1
.= bool ((A . i) \+\ (B . i)) by A1, PBOOLE:4 ;
::_thesis: verum
end;

theorem Th1: :: MBOOLEAN:1
for I being set
for X, Y being ManySortedSet of I holds
( X = bool Y iff for A being ManySortedSet of I holds
( A in X iff A c= Y ) )
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds
( X = bool Y iff for A being ManySortedSet of I holds
( A in X iff A c= Y ) )
let X, Y be ManySortedSet of I; ::_thesis: ( X = bool Y iff for A being ManySortedSet of I holds
( A in X iff A c= Y ) )
thus  ( X = bool Y implies for A being ManySortedSet of I holds
( A in X iff A c= Y ) ) ::_thesis: ( ( for A being ManySortedSet of I holds
( A in X iff A c= Y ) ) implies X = bool Y )
proof
assume A1: X = bool Y ; ::_thesis: for A being ManySortedSet of I holds
( A in X iff A c= Y )
let A be ManySortedSet of I; ::_thesis: ( A in X iff A c= Y )
thus  ( A in X implies A c= Y ) ::_thesis: ( A c= Y implies A in X )
proof
assume A2: A in X ; ::_thesis: A c= Y
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= Y . i )
assume A3: i in I ; ::_thesis: A . i c= Y . i
then A4: A . i in X . i by A2, PBOOLE:def_1;
 X . i = bool (Y . i) by A1, A3, Def1;
hence  A . i c= Y . i by A4; ::_thesis: verum
end;
assume A5: A c= Y ; ::_thesis: A in X
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in X . i )
assume A6: i in I ; ::_thesis: A . i in X . i
then A7: A . i c= Y . i by A5, PBOOLE:def_2;
 X . i = bool (Y . i) by A1, A6, Def1;
hence  A . i in X . i by A7; ::_thesis: verum
end;
assume A8: for A being ManySortedSet of I holds
( A in X iff A c= Y ) ; ::_thesis: X = bool Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_(bool_Y)_._i
let i be set ; ::_thesis: ( i in I implies X . i = (bool Y) . i )
assume A9: i in I ; ::_thesis: X . i = (bool Y) . i
 [[0]] I c= Y by PBOOLE:43;
then A10: [[0]] I in X by A8;
 for A9 being set holds
( A9 in X . i iff A9 c= Y . i )
proof
let A9 be set ; ::_thesis: ( A9 in X . i iff A9 c= Y . i )
A11: dom (i .--> A9) = {i} by FUNCOP_1:13;
 dom (([[0]] I) +* (i .--> A9)) = I by A9, Lm1;
then reconsider K = ([[0]] I) +* (i .--> A9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
 i in {i} by TARSKI:def_1;
then A12: K . i = (i .--> A9) . i by A11, FUNCT_4:13
.= A9 by FUNCOP_1:72 ;
thus  ( A9 in X . i implies A9 c= Y . i ) ::_thesis: ( A9 c= Y . i implies A9 in X . i )
proof
assume A13: A9 in X . i ; ::_thesis: A9 c= Y . i
 K in X
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in X . j )
assume A14: j in I ; ::_thesis: K . j in X . j
now__::_thesis:_(_(_j_=_i_&_K_._j_in_X_._j_)_or_(_j_<>_i_&_K_._j_in_X_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K . j in X . j
hence  K . j in X . j by A12, A13; ::_thesis: verum
end;
case j <> i ; ::_thesis: K . j in X . j
then  not j in dom (i .--> A9) by A11, TARSKI:def_1;
then  K . j = ([[0]] I) . j by FUNCT_4:11;
hence  K . j in X . j by A10, A14, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  K . j in X . j ; ::_thesis: verum
end;
then  K c= Y by A8;
hence  A9 c= Y . i by A9, A12, PBOOLE:def_2; ::_thesis: verum
end;
assume A15: A9 c= Y . i ; ::_thesis: A9 in X . i
 K c= Y
proof
let j be set ; :: according to PBOOLE:def_2 ::_thesis: ( not j in I or K . j c= Y . j )
assume A16: j in I ; ::_thesis: K . j c= Y . j
now__::_thesis:_(_(_j_=_i_&_K_._j_c=_Y_._j_)_or_(_j_<>_i_&_K_._j_c=_Y_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K . j c= Y . j
hence  K . j c= Y . j by A12, A15; ::_thesis: verum
end;
case j <> i ; ::_thesis: K . j c= Y . j
then  not j in dom (i .--> A9) by A11, TARSKI:def_1;
then A17: K . j = ([[0]] I) . j by FUNCT_4:11;
 [[0]] I c= Y by PBOOLE:43;
hence  K . j c= Y . j by A16, A17, PBOOLE:def_2; ::_thesis: verum
end;
end;
end;
hence  K . j c= Y . j ; ::_thesis: verum
end;
then  K in X by A8;
hence  A9 in X . i by A9, A12, PBOOLE:def_1; ::_thesis: verum
end;
then  X . i = bool (Y . i) by ZFMISC_1:def_1;
hence  X . i = (bool Y) . i by A9, Def1; ::_thesis: verum
end;
hence  X = bool Y by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:2
for I being set holds bool ([[0]] I) = I --> {{}}
proof
let I be set ; ::_thesis: bool ([[0]] I) = I --> {{}}
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(bool_([[0]]_I))_._i_=_(I_-->_{{}})_._i
let i be set ; ::_thesis: ( i in I implies (bool ([[0]] I)) . i = (I --> {{}}) . i )
assume A1: i in I ; ::_thesis: (bool ([[0]] I)) . i = (I --> {{}}) . i
then (bool ([[0]] I)) . i = bool (([[0]] I) . i) by Def1
.= {{}} by PBOOLE:5, ZFMISC_1:1 ;
hence  (bool ([[0]] I)) . i = (I --> {{}}) . i by A1, FUNCOP_1:7; ::_thesis: verum
end;
hence  bool ([[0]] I) = I --> {{}} by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:3
for I, x being set holds bool (I --> x) = I --> (bool x)
proof
let I, x be set ; ::_thesis: bool (I --> x) = I --> (bool x)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(bool_(I_-->_x))_._i_=_(I_-->_(bool_x))_._i
let i be set ; ::_thesis: ( i in I implies (bool (I --> x)) . i = (I --> (bool x)) . i )
assume A1: i in I ; ::_thesis: (bool (I --> x)) . i = (I --> (bool x)) . i
hence (bool (I --> x)) . i = bool ((I --> x) . i) by Def1
.= bool x by A1, FUNCOP_1:7
.= (I --> (bool x)) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence  bool (I --> x) = I --> (bool x) by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:4
for I, x being set holds bool (I --> {x}) = I --> {{},{x}}
proof
let I, x be set ; ::_thesis: bool (I --> {x}) = I --> {{},{x}}
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(bool_(I_-->_{x}))_._i_=_(I_-->_{{},{x}})_._i
let i be set ; ::_thesis: ( i in I implies (bool (I --> {x})) . i = (I --> {{},{x}}) . i )
assume A1: i in I ; ::_thesis: (bool (I --> {x})) . i = (I --> {{},{x}}) . i
hence (bool (I --> {x})) . i = bool ((I --> {x}) . i) by Def1
.= bool {x} by A1, FUNCOP_1:7
.= {{},{x}} by ZFMISC_1:24
.= (I --> {{},{x}}) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence  bool (I --> {x}) = I --> {{},{x}} by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:5
for I being set
for A being ManySortedSet of I holds [[0]] I c= A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds [[0]] I c= A
let A be ManySortedSet of I; ::_thesis: [[0]] I c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ([[0]] I) . i c= A . i )
assume  i in I ; ::_thesis: ([[0]] I) . i c= A . i
 ([[0]] I) . i = {} by PBOOLE:5;
hence  ([[0]] I) . i c= A . i by XBOOLE_1:2; ::_thesis: verum
end;

theorem :: MBOOLEAN:6
for I being set
for A, B being ManySortedSet of I st A c= B holds
bool A c= bool B
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A c= B holds
bool A c= bool B
let A, B be ManySortedSet of I; ::_thesis: ( A c= B implies bool A c= bool B )
assume A1: A c= B ; ::_thesis: bool A c= bool B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (bool A) . i c= (bool B) . i )
assume A2: i in I ; ::_thesis: (bool A) . i c= (bool B) . i
then A3: A . i c= B . i by A1, PBOOLE:def_2;
 ( (bool A) . i = bool (A . i) & (bool B) . i = bool (B . i) ) by A2, Def1;
hence  (bool A) . i c= (bool B) . i by A3, ZFMISC_1:67; ::_thesis: verum
end;

theorem :: MBOOLEAN:7
for I being set
for A, B being ManySortedSet of I holds (bool A) \/ (bool B) c= bool (A \/ B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (bool A) \/ (bool B) c= bool (A \/ B)
let A, B be ManySortedSet of I; ::_thesis: (bool A) \/ (bool B) c= bool (A \/ B)
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i )
assume A1: i in I ; ::_thesis: ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i
then A2: (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) by Lm2;
((bool A) \/ (bool B)) . i = ((bool A) . i) \/ ((bool B) . i) by A1, PBOOLE:def_4
.= (bool (A . i)) \/ ((bool B) . i) by A1, Def1
.= (bool (A . i)) \/ (bool (B . i)) by A1, Def1 ;
hence  ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i by A2, ZFMISC_1:69; ::_thesis: verum
end;

theorem :: MBOOLEAN:8
for I being set
for A, B being ManySortedSet of I st (bool A) \/ (bool B) = bool (A \/ B) holds
for i being set st i in I holds
A . i,B . i are_c=-comparable
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st (bool A) \/ (bool B) = bool (A \/ B) holds
for i being set st i in I holds
A . i,B . i are_c=-comparable
let A, B be ManySortedSet of I; ::_thesis: ( (bool A) \/ (bool B) = bool (A \/ B) implies for i being set st i in I holds
A . i,B . i are_c=-comparable )
assume A1: (bool A) \/ (bool B) = bool (A \/ B) ; ::_thesis: for i being set st i in I holds
A . i,B . i are_c=-comparable
let i be set ; ::_thesis: ( i in I implies A . i,B . i are_c=-comparable )
assume A2: i in I ; ::_thesis: A . i,B . i are_c=-comparable
bool ((A . i) \/ (B . i)) = ((bool A) \/ (bool B)) . i by A1, A2, Lm2
.= ((bool A) . i) \/ ((bool B) . i) by A2, PBOOLE:def_4
.= ((bool A) . i) \/ (bool (B . i)) by A2, Def1
.= (bool (A . i)) \/ (bool (B . i)) by A2, Def1 ;
hence  A . i,B . i are_c=-comparable by ZFMISC_1:70; ::_thesis: verum
end;

theorem :: MBOOLEAN:9
for I being set
for A, B being ManySortedSet of I holds bool (A /\ B) = (bool A) /\ (bool B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds bool (A /\ B) = (bool A) /\ (bool B)
let A, B be ManySortedSet of I; ::_thesis: bool (A /\ B) = (bool A) /\ (bool B)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(bool_(A_/\_B))_._i_=_((bool_A)_/\_(bool_B))_._i
let i be set ; ::_thesis: ( i in I implies (bool (A /\ B)) . i = ((bool A) /\ (bool B)) . i )
assume A1: i in I ; ::_thesis: (bool (A /\ B)) . i = ((bool A) /\ (bool B)) . i
hence (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) by Lm3
.= (bool (A . i)) /\ (bool (B . i)) by ZFMISC_1:71
.= (bool (A . i)) /\ ((bool B) . i) by A1, Def1
.= ((bool A) . i) /\ ((bool B) . i) by A1, Def1
.= ((bool A) /\ (bool B)) . i by A1, PBOOLE:def_5 ;
::_thesis: verum
end;
hence  bool (A /\ B) = (bool A) /\ (bool B) by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:10
for I being set
for A, B being ManySortedSet of I holds bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B))
let A, B be ManySortedSet of I; ::_thesis: bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B))
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i )
assume A1: i in I ; ::_thesis: (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i
then A2: (bool (A \ B)) . i = bool ((A . i) \ (B . i)) by Lm4;
((I --> {{}}) \/ ((bool A) \ (bool B))) . i = ((I --> {{}}) . i) \/ (((bool A) \ (bool B)) . i) by A1, PBOOLE:def_4
.= {{}} \/ (((bool A) \ (bool B)) . i) by A1, FUNCOP_1:7
.= {{}} \/ (((bool A) . i) \ ((bool B) . i)) by A1, PBOOLE:def_6
.= {{}} \/ ((bool (A . i)) \ ((bool B) . i)) by A1, Def1
.= {{}} \/ ((bool (A . i)) \ (bool (B . i))) by A1, Def1 ;
hence  (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i by A2, ZFMISC_1:72; ::_thesis: verum
end;

theorem :: MBOOLEAN:11
for I being set
for X, A, B being ManySortedSet of I holds
( X c= A \ B iff ( X c= A & X misses B ) )
proof
let I be set ; ::_thesis: for X, A, B being ManySortedSet of I holds
( X c= A \ B iff ( X c= A & X misses B ) )
let X, A, B be ManySortedSet of I; ::_thesis: ( X c= A \ B iff ( X c= A & X misses B ) )
thus  ( X c= A \ B implies ( X c= A & X misses B ) ) ::_thesis: ( X c= A & X misses B implies X c= A \ B )
proof
assume  X c= A \ B ; ::_thesis: ( X c= A & X misses B )
then A1: X in bool (A \ B) by Th1;
thus  X c= A ::_thesis: X misses B
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i )
assume A2: i in I ; ::_thesis: X . i c= A . i
then  X . i in (bool (A \ B)) . i by A1, PBOOLE:def_1;
then  X . i in bool ((A . i) \ (B . i)) by A2, Lm4;
hence  X . i c= A . i by XBOOLE_1:106; ::_thesis: verum
end;
let i be set ; :: according to PBOOLE:def_8 ::_thesis: ( not i in I or X . i misses B . i )
assume A3: i in I ; ::_thesis: X . i misses B . i
then  X . i in (bool (A \ B)) . i by A1, PBOOLE:def_1;
then  X . i in bool ((A . i) \ (B . i)) by A3, Lm4;
hence  X . i misses B . i by XBOOLE_1:106; ::_thesis: verum
end;
assume A4: ( X c= A & X misses B ) ; ::_thesis: X c= A \ B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \ B) . i )
assume A5: i in I ; ::_thesis: X . i c= (A \ B) . i
then  ( X . i c= A . i & X . i misses B . i ) by A4, PBOOLE:def_2, PBOOLE:def_8;
then  X . i c= (A . i) \ (B . i) by XBOOLE_1:86;
hence  X . i c= (A \ B) . i by A5, PBOOLE:def_6; ::_thesis: verum
end;

theorem :: MBOOLEAN:12
for I being set
for A, B being ManySortedSet of I holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
let A, B be ManySortedSet of I; ::_thesis: (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i )
assume A1: i in I ; ::_thesis: ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i
then A2: (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) by Lm5;
((bool (A \ B)) \/ (bool (B \ A))) . i = ((bool (A \ B)) . i) \/ ((bool (B \ A)) . i) by A1, PBOOLE:def_4
.= (bool ((A . i) \ (B . i))) \/ ((bool (B \ A)) . i) by A1, Lm4
.= (bool ((A . i) \ (B . i))) \/ (bool ((B . i) \ (A . i))) by A1, Lm4 ;
hence  ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i by A2, ZFMISC_1:73; ::_thesis: verum
end;

theorem :: MBOOLEAN:13
for I being set
for X, A, B being ManySortedSet of I holds
( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
proof
let I be set ; ::_thesis: for X, A, B being ManySortedSet of I holds
( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
let X, A, B be ManySortedSet of I; ::_thesis: ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
thus  ( X c= A \+\ B implies ( X c= A \/ B & X misses A /\ B ) ) ::_thesis: ( X c= A \/ B & X misses A /\ B implies X c= A \+\ B )
proof
assume  X c= A \+\ B ; ::_thesis: ( X c= A \/ B & X misses A /\ B )
then A1: X in bool (A \+\ B) by Th1;
thus  X c= A \/ B ::_thesis: X misses A /\ B
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \/ B) . i )
assume A2: i in I ; ::_thesis: X . i c= (A \/ B) . i
then  X . i in (bool (A \+\ B)) . i by A1, PBOOLE:def_1;
then  X . i in bool ((A . i) \+\ (B . i)) by A2, Lm5;
then  X . i c= (A . i) \/ (B . i) by XBOOLE_1:107;
hence  X . i c= (A \/ B) . i by A2, PBOOLE:def_4; ::_thesis: verum
end;
let i be set ; :: according to PBOOLE:def_8 ::_thesis: ( not i in I or X . i misses (A /\ B) . i )
assume A3: i in I ; ::_thesis: X . i misses (A /\ B) . i
then  X . i in (bool (A \+\ B)) . i by A1, PBOOLE:def_1;
then  X . i in bool ((A . i) \+\ (B . i)) by A3, Lm5;
then  X . i misses (A . i) /\ (B . i) by XBOOLE_1:107;
hence  X . i misses (A /\ B) . i by A3, PBOOLE:def_5; ::_thesis: verum
end;
assume that
A4: X c= A \/ B and
A5: X misses A /\ B ; ::_thesis: X c= A \+\ B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \+\ B) . i )
assume A6: i in I ; ::_thesis: X . i c= (A \+\ B) . i
then  X . i misses (A /\ B) . i by A5, PBOOLE:def_8;
then A7: X . i misses (A . i) /\ (B . i) by A6, PBOOLE:def_5;
 X . i c= (A \/ B) . i by A4, A6, PBOOLE:def_2;
then  X . i c= (A . i) \/ (B . i) by A6, PBOOLE:def_4;
then  X . i c= (A . i) \+\ (B . i) by A7, XBOOLE_1:107;
hence  X . i c= (A \+\ B) . i by A6, PBOOLE:4; ::_thesis: verum
end;

theorem :: MBOOLEAN:14
for I being set
for X, A, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds
X /\ Y c= A
proof
let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds
X /\ Y c= A
let X, A, Y be ManySortedSet of I; ::_thesis: ( ( X c= A or Y c= A ) implies X /\ Y c= A )
assume A1: ( X c= A or Y c= A ) ; ::_thesis: X /\ Y c= A
percases ( X c= A or Y c= A ) by A1;
supposeA2: X c= A ; ::_thesis: X /\ Y c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X /\ Y) . i c= A . i )
assume A3: i in I ; ::_thesis: (X /\ Y) . i c= A . i
then  X . i c= A . i by A2, PBOOLE:def_2;
then  (X . i) /\ (Y . i) c= A . i by XBOOLE_1:108;
hence  (X /\ Y) . i c= A . i by A3, PBOOLE:def_5; ::_thesis: verum
end;
supposeA4: Y c= A ; ::_thesis: X /\ Y c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X /\ Y) . i c= A . i )
assume A5: i in I ; ::_thesis: (X /\ Y) . i c= A . i
then  Y . i c= A . i by A4, PBOOLE:def_2;
then  (X . i) /\ (Y . i) c= A . i by XBOOLE_1:108;
hence  (X /\ Y) . i c= A . i by A5, PBOOLE:def_5; ::_thesis: verum
end;
end;
end;

theorem :: MBOOLEAN:15
for I being set
for X, A, Y being ManySortedSet of I st X c= A holds
X \ Y c= A
proof
let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st X c= A holds
X \ Y c= A
let X, A, Y be ManySortedSet of I; ::_thesis: ( X c= A implies X \ Y c= A )
assume A1: X c= A ; ::_thesis: X \ Y c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X \ Y) . i c= A . i )
assume A2: i in I ; ::_thesis: (X \ Y) . i c= A . i
then  X . i c= A . i by A1, PBOOLE:def_2;
then  (X . i) \ (Y . i) c= A . i by XBOOLE_1:109;
hence  (X \ Y) . i c= A . i by A2, PBOOLE:def_6; ::_thesis: verum
end;

theorem :: MBOOLEAN:16
for I being set
for X, A, Y being ManySortedSet of I st X c= A & Y c= A holds
X \+\ Y c= A
proof
let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st X c= A & Y c= A holds
X \+\ Y c= A
let X, A, Y be ManySortedSet of I; ::_thesis: ( X c= A & Y c= A implies X \+\ Y c= A )
assume A1: ( X c= A & Y c= A ) ; ::_thesis: X \+\ Y c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X \+\ Y) . i c= A . i )
assume A2: i in I ; ::_thesis: (X \+\ Y) . i c= A . i
then  ( X . i c= A . i & Y . i c= A . i ) by A1, PBOOLE:def_2;
then  (X . i) \+\ (Y . i) c= A . i by XBOOLE_1:110;
then  (X . i) \+\ (Y . i) in bool (A . i) ;
then  (X \+\ Y) . i in bool (A . i) by A2, PBOOLE:4;
hence  (X \+\ Y) . i c= A . i ; ::_thesis: verum
end;

theorem :: MBOOLEAN:17
for I being set
for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X \/ Y))
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X \/ Y))
let X, Y be ManySortedSet of I; ::_thesis: [|X,Y|] c= bool (bool (X \/ Y))
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or [|X,Y|] . i c= (bool (bool (X \/ Y))) . i )
assume A1: i in I ; ::_thesis: [|X,Y|] . i c= (bool (bool (X \/ Y))) . i
then A2: [|X,Y|] . i = [:(X . i),(Y . i):] by PBOOLE:def_16;
(bool (bool (X \/ Y))) . i = bool ((bool (X \/ Y)) . i) by A1, Def1
.= bool (bool ((X . i) \/ (Y . i))) by A1, Lm2 ;
hence  [|X,Y|] . i c= (bool (bool (X \/ Y))) . i by A2, ZFMISC_1:86; ::_thesis: verum
end;

theorem :: MBOOLEAN:18
for I being set
for X, A being ManySortedSet of I holds
( X c= A iff X in bool A )
proof
let I be set ; ::_thesis: for X, A being ManySortedSet of I holds
( X c= A iff X in bool A )
let X, A be ManySortedSet of I; ::_thesis: ( X c= A iff X in bool A )
thus  ( X c= A implies X in bool A ) ::_thesis: ( X in bool A implies X c= A )
proof
assume A1: X c= A ; ::_thesis: X in bool A
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or X . i in (bool A) . i )
assume A2: i in I ; ::_thesis: X . i in (bool A) . i
then  X . i c= A . i by A1, PBOOLE:def_2;
then  X . i in bool (A . i) ;
hence  X . i in (bool A) . i by A2, Def1; ::_thesis: verum
end;
assume A3: X in bool A ; ::_thesis: X c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i )
assume A4: i in I ; ::_thesis: X . i c= A . i
then  X . i in (bool A) . i by A3, PBOOLE:def_1;
then  X . i in bool (A . i) by A4, Def1;
hence  X . i c= A . i ; ::_thesis: verum
end;

theorem :: MBOOLEAN:19
for I being set
for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|]
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|]
let A, B be ManySortedSet of I; ::_thesis: (Funcs) (A,B) c= bool [|A,B|]
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i )
assume A1: i in I ; ::_thesis: ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i
then A2: ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def_17;
(bool [|A,B|]) . i = bool ([|A,B|] . i) by A1, Def1
.= bool [:(A . i),(B . i):] by A1, PBOOLE:def_16 ;
hence  ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i by A2, FRAENKEL:2; ::_thesis: verum
end;

begin

definition
let I be set ;
let A be ManySortedSet of I;
func union A ->  ManySortedSet of I means :Def2: :: MBOOLEAN:def 2
 for i being set st i in I holds
it . i = union (A . i);
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = union (A . i)
proof
deffunc H1( set ) ->  set = union (A . $1);
thus  ex X being ManySortedSet of I st
for i being set st i in I holds
X . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = union (A . i) ) & ( for i being set st i in I holds
b2 . i = union (A . i) ) holds
b1 = b2
proof
let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
X . i = union (A . i) ) & ( for i being set st i in I holds
Y . i = union (A . i) ) implies X = Y )
assume that
A1: for i being set st i in I holds
X . i = union (A . i) and
A2: for i being set st i in I holds
Y . i = union (A . i) ; ::_thesis: X = Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_Y_._i
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume A3: i in I ; ::_thesis: X . i = Y . i
hence X . i = union (A . i) by A1
.= Y . i by A2, A3 ;
::_thesis: verum
end;
hence  X = Y by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines union MBOOLEAN:def_2_:_
 for I being set
for A, b3 being ManySortedSet of I holds
( b3 = union A iff for i being set st i in I holds
b3 . i = union (A . i) );

registration
let I be set ;
cluster union ([[0]] I) -> V3() ;
coherence
 union ([[0]] I) is empty-yielding
proof
let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( not i in I or (union ([[0]] I)) . i is empty )
A1: union (([[0]] I) . i) is empty by PBOOLE:5, ZFMISC_1:2;
assume  i in I ; ::_thesis: (union ([[0]] I)) . i is empty
hence  (union ([[0]] I)) . i is empty by A1, Def2; ::_thesis: verum
end;
end;

Lm6:  for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A \/ B)) . i = union ((A . i) \/ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A \/ B)) . i = union ((A . i) \/ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(union (A \/ B)) . i = union ((A . i) \/ (B . i))
let i be set ; ::_thesis: ( i in I implies (union (A \/ B)) . i = union ((A . i) \/ (B . i)) )
assume A1: i in I ; ::_thesis: (union (A \/ B)) . i = union ((A . i) \/ (B . i))
hence (union (A \/ B)) . i = union ((A \/ B) . i) by Def2
.= union ((A . i) \/ (B . i)) by A1, PBOOLE:def_4 ;
::_thesis: verum
end;

Lm7:  for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A /\ B)) . i = union ((A . i) /\ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A /\ B)) . i = union ((A . i) /\ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(union (A /\ B)) . i = union ((A . i) /\ (B . i))
let i be set ; ::_thesis: ( i in I implies (union (A /\ B)) . i = union ((A . i) /\ (B . i)) )
assume A1: i in I ; ::_thesis: (union (A /\ B)) . i = union ((A . i) /\ (B . i))
hence (union (A /\ B)) . i = union ((A /\ B) . i) by Def2
.= union ((A . i) /\ (B . i)) by A1, PBOOLE:def_5 ;
::_thesis: verum
end;

theorem :: MBOOLEAN:20
for I being set
for A, X being ManySortedSet of I holds
( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
proof
let I be set ; ::_thesis: for A, X being ManySortedSet of I holds
( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
let A, X be ManySortedSet of I; ::_thesis: ( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
thus  ( A in union X implies ex Y being ManySortedSet of I st
( A in Y & Y in X ) ) ::_thesis: ( ex Y being ManySortedSet of I st
( A in Y & Y in X ) implies A in union X )
proof
defpred S1[ set , set ] means ( A . $1 in $2 & $2 in X . $1 );
assume A1: A in union X ; ::_thesis: ex Y being ManySortedSet of I st
( A in Y & Y in X )
A2: for i being set st i in I holds
ex Y being set st S1[i,Y]
proof
let i be set ; ::_thesis: ( i in I implies ex Y being set st S1[i,Y] )
assume A3: i in I ; ::_thesis: ex Y being set st S1[i,Y]
then  A . i in (union X) . i by A1, PBOOLE:def_1;
then  A . i in union (X . i) by A3, Def2;
hence  ex Y being set st S1[i,Y] by TARSKI:def_4; ::_thesis: verum
end;
consider K being ManySortedSet of I such that
A4: for i being set st i in I holds
S1[i,K . i] from PBOOLE:sch_3(A2);
take  K ; ::_thesis: ( A in K & K in X )
thus  A in K ::_thesis: K in X
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in K . i )
assume  i in I ; ::_thesis: A . i in K . i
hence  A . i in K . i by A4; ::_thesis: verum
end;
thus  K in X ::_thesis: verum
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or K . i in X . i )
assume  i in I ; ::_thesis: K . i in X . i
hence  K . i in X . i by A4; ::_thesis: verum
end;
end;
given Y being ManySortedSet of I such that A5: ( A in Y & Y in X ) ; ::_thesis: A in union X
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in (union X) . i )
assume A6: i in I ; ::_thesis: A . i in (union X) . i
then  ( A . i in Y . i & Y . i in X . i ) by A5, PBOOLE:def_1;
then  A . i in union (X . i) by TARSKI:def_4;
hence  A . i in (union X) . i by A6, Def2; ::_thesis: verum
end;

theorem :: MBOOLEAN:21
for I being set holds union ([[0]] I) = [[0]] I
proof
let I be set ; ::_thesis: union ([[0]] I) = [[0]] I
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_([[0]]_I))_._i_=_([[0]]_I)_._i
let i be set ; ::_thesis: ( i in I implies (union ([[0]] I)) . i = ([[0]] I) . i )
assume  i in I ; ::_thesis: (union ([[0]] I)) . i = ([[0]] I) . i
hence (union ([[0]] I)) . i = union (([[0]] I) . i) by Def2
.= {} by PBOOLE:5, ZFMISC_1:2
.= ([[0]] I) . i by PBOOLE:5 ;
::_thesis: verum
end;
hence  union ([[0]] I) = [[0]] I by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:22
for I, x being set holds union (I --> x) = I --> (union x)
proof
let I, x be set ; ::_thesis: union (I --> x) = I --> (union x)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(I_-->_x))_._i_=_(I_-->_(union_x))_._i
let i be set ; ::_thesis: ( i in I implies (union (I --> x)) . i = (I --> (union x)) . i )
assume A1: i in I ; ::_thesis: (union (I --> x)) . i = (I --> (union x)) . i
hence (union (I --> x)) . i = union ((I --> x) . i) by Def2
.= union x by A1, FUNCOP_1:7
.= (I --> (union x)) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence  union (I --> x) = I --> (union x) by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:23
for I, x being set holds union (I --> {x}) = I --> x
proof
let I, x be set ; ::_thesis: union (I --> {x}) = I --> x
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(I_-->_{x}))_._i_=_(I_-->_x)_._i
let i be set ; ::_thesis: ( i in I implies (union (I --> {x})) . i = (I --> x) . i )
assume A1: i in I ; ::_thesis: (union (I --> {x})) . i = (I --> x) . i
hence (union (I --> {x})) . i = union ((I --> {x}) . i) by Def2
.= union {x} by A1, FUNCOP_1:7
.= x by ZFMISC_1:25
.= (I --> x) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence  union (I --> {x}) = I --> x by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:24
for I, x, y being set holds union (I --> {{x},{y}}) = I --> {x,y}
proof
let I, x, y be set ; ::_thesis: union (I --> {{x},{y}}) = I --> {x,y}
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(I_-->_{{x},{y}}))_._i_=_(I_-->_{x,y})_._i
let i be set ; ::_thesis: ( i in I implies (union (I --> {{x},{y}})) . i = (I --> {x,y}) . i )
assume A1: i in I ; ::_thesis: (union (I --> {{x},{y}})) . i = (I --> {x,y}) . i
hence (union (I --> {{x},{y}})) . i = union ((I --> {{x},{y}}) . i) by Def2
.= union {{x},{y}} by A1, FUNCOP_1:7
.= {x,y} by ZFMISC_1:26
.= (I --> {x,y}) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence  union (I --> {{x},{y}}) = I --> {x,y} by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:25
for I being set
for X, A being ManySortedSet of I st X in A holds
X c= union A
proof
let I be set ; ::_thesis: for X, A being ManySortedSet of I st X in A holds
X c= union A
let X, A be ManySortedSet of I; ::_thesis: ( X in A implies X c= union A )
assume A1: X in A ; ::_thesis: X c= union A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (union A) . i )
assume A2: i in I ; ::_thesis: X . i c= (union A) . i
then  X . i in A . i by A1, PBOOLE:def_1;
then  X . i c= union (A . i) by ZFMISC_1:74;
hence  X . i c= (union A) . i by A2, Def2; ::_thesis: verum
end;

theorem :: MBOOLEAN:26
for I being set
for A, B being ManySortedSet of I st A c= B holds
union A c= union B
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A c= B holds
union A c= union B
let A, B be ManySortedSet of I; ::_thesis: ( A c= B implies union A c= union B )
assume A1: A c= B ; ::_thesis: union A c= union B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union A) . i c= (union B) . i )
assume A2: i in I ; ::_thesis: (union A) . i c= (union B) . i
then  A . i c= B . i by A1, PBOOLE:def_2;
then  union (A . i) c= union (B . i) by ZFMISC_1:77;
then  (union A) . i c= union (B . i) by A2, Def2;
hence  (union A) . i c= (union B) . i by A2, Def2; ::_thesis: verum
end;

theorem :: MBOOLEAN:27
for I being set
for A, B being ManySortedSet of I holds union (A \/ B) = (union A) \/ (union B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds union (A \/ B) = (union A) \/ (union B)
let A, B be ManySortedSet of I; ::_thesis: union (A \/ B) = (union A) \/ (union B)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(A_\/_B))_._i_=_((union_A)_\/_(union_B))_._i
let i be set ; ::_thesis: ( i in I implies (union (A \/ B)) . i = ((union A) \/ (union B)) . i )
assume A1: i in I ; ::_thesis: (union (A \/ B)) . i = ((union A) \/ (union B)) . i
hence (union (A \/ B)) . i = union ((A . i) \/ (B . i)) by Lm6
.= (union (A . i)) \/ (union (B . i)) by ZFMISC_1:78
.= ((union A) . i) \/ (union (B . i)) by A1, Def2
.= ((union A) . i) \/ ((union B) . i) by A1, Def2
.= ((union A) \/ (union B)) . i by A1, PBOOLE:def_4 ;
::_thesis: verum
end;
hence  union (A \/ B) = (union A) \/ (union B) by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:28
for I being set
for A, B being ManySortedSet of I holds union (A /\ B) c= (union A) /\ (union B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds union (A /\ B) c= (union A) /\ (union B)
let A, B be ManySortedSet of I; ::_thesis: union (A /\ B) c= (union A) /\ (union B)
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union (A /\ B)) . i c= ((union A) /\ (union B)) . i )
assume A1: i in I ; ::_thesis: (union (A /\ B)) . i c= ((union A) /\ (union B)) . i
then A2: (union (A /\ B)) . i = union ((A . i) /\ (B . i)) by Lm7;
((union A) /\ (union B)) . i = ((union A) . i) /\ ((union B) . i) by A1, PBOOLE:def_5
.= (union (A . i)) /\ ((union B) . i) by A1, Def2
.= (union (A . i)) /\ (union (B . i)) by A1, Def2 ;
hence  (union (A /\ B)) . i c= ((union A) /\ (union B)) . i by A2, ZFMISC_1:79; ::_thesis: verum
end;

theorem :: MBOOLEAN:29
for I being set
for A being ManySortedSet of I holds union (bool A) = A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds union (bool A) = A
let A be ManySortedSet of I; ::_thesis: union (bool A) = A
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(bool_A))_._i_=_A_._i
let i be set ; ::_thesis: ( i in I implies (union (bool A)) . i = A . i )
assume A1: i in I ; ::_thesis: (union (bool A)) . i = A . i
hence (union (bool A)) . i = union ((bool A) . i) by Def2
.= union (bool (A . i)) by A1, Def1
.= A . i by ZFMISC_1:81 ;
::_thesis: verum
end;
hence  union (bool A) = A by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:30
for I being set
for A being ManySortedSet of I holds A c= bool (union A)
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds A c= bool (union A)
let A be ManySortedSet of I; ::_thesis: A c= bool (union A)
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= (bool (union A)) . i )
assume A1: i in I ; ::_thesis: A . i c= (bool (union A)) . i
then (bool (union A)) . i = bool ((union A) . i) by Def1
.= bool (union (A . i)) by A1, Def2 ;
hence  A . i c= (bool (union A)) . i by ZFMISC_1:82; ::_thesis: verum
end;

theorem :: MBOOLEAN:31
for I being set
for Y, A, X being ManySortedSet of I st union Y c= A & X in Y holds
X c= A
proof
let I be set ; ::_thesis: for Y, A, X being ManySortedSet of I st union Y c= A & X in Y holds
X c= A
let Y, A, X be ManySortedSet of I; ::_thesis: ( union Y c= A & X in Y implies X c= A )
assume that
A1: union Y c= A and
A2: X in Y ; ::_thesis: X c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i )
assume A3: i in I ; ::_thesis: X . i c= A . i
then  (union Y) . i c= A . i by A1, PBOOLE:def_2;
then A4: union (Y . i) c= A . i by A3, Def2;
 X . i in Y . i by A2, A3, PBOOLE:def_1;
hence  X . i c= A . i by A4, SETFAM_1:41; ::_thesis: verum
end;

theorem :: MBOOLEAN:32
for I being set
for Z being ManySortedSet of I
for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X c= Z ) holds
union A c= Z
proof
let I be set ; ::_thesis: for Z being ManySortedSet of I
for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X c= Z ) holds
union A c= Z
let Z be ManySortedSet of I; ::_thesis: for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X c= Z ) holds
union A c= Z
let A be V2() ManySortedSet of I; ::_thesis: ( ( for X being ManySortedSet of I st X in A holds
X c= Z ) implies union A c= Z )
assume A1: for X being ManySortedSet of I st X in A holds
X c= Z ; ::_thesis: union A c= Z
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union A) . i c= Z . i )
assume A2: i in I ; ::_thesis: (union A) . i c= Z . i
 for X9 being set st X9 in A . i holds
X9 c= Z . i
proof
consider M being ManySortedSet of I such that
A3: M in A by PBOOLE:134;
let X9 be set ; ::_thesis: ( X9 in A . i implies X9 c= Z . i )
assume A4: X9 in A . i ; ::_thesis: X9 c= Z . i
 dom (M +* (i .--> X9)) = I by A2, Lm1;
then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> X9) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A6: K . i = (i .--> X9) . i by A5, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
 K in A
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in A . j )
assume A7: j in I ; ::_thesis: K . j in A . j
now__::_thesis:_(_(_j_=_i_&_K_._j_in_A_._j_)_or_(_j_<>_i_&_K_._j_in_A_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K . j in A . j
hence  K . j in A . j by A4, A6; ::_thesis: verum
end;
case j <> i ; ::_thesis: K . j in A . j
then  not j in dom (i .--> X9) by A5, TARSKI:def_1;
then  K . j = M . j by FUNCT_4:11;
hence  K . j in A . j by A3, A7, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  K . j in A . j ; ::_thesis: verum
end;
then  K c= Z by A1;
hence  X9 c= Z . i by A2, A6, PBOOLE:def_2; ::_thesis: verum
end;
then  union (A . i) c= Z . i by ZFMISC_1:76;
hence  (union A) . i c= Z . i by A2, Def2; ::_thesis: verum
end;

theorem :: MBOOLEAN:33
for I being set
for B being ManySortedSet of I
for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ) holds
(union A) /\ B = [[0]] I
proof
let I be set ; ::_thesis: for B being ManySortedSet of I
for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ) holds
(union A) /\ B = [[0]] I
let B be ManySortedSet of I; ::_thesis: for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ) holds
(union A) /\ B = [[0]] I
let A be V2() ManySortedSet of I; ::_thesis: ( ( for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ) implies (union A) /\ B = [[0]] I )
assume A1: for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ; ::_thesis: (union A) /\ B = [[0]] I
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
((union_A)_/\_B)_._i_=_([[0]]_I)_._i
let i be set ; ::_thesis: ( i in I implies ((union A) /\ B) . i = ([[0]] I) . i )
assume A2: i in I ; ::_thesis: ((union A) /\ B) . i = ([[0]] I) . i
 for X9 being set st X9 in A . i holds
X9 misses B . i
proof
consider M being ManySortedSet of I such that
A3: M in A by PBOOLE:134;
let X9 be set ; ::_thesis: ( X9 in A . i implies X9 misses B . i )
assume A4: X9 in A . i ; ::_thesis: X9 misses B . i
 dom (M +* (i .--> X9)) = I by A2, Lm1;
then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> X9) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A6: K . i = (i .--> X9) . i by A5, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
 K in A
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in A . j )
assume A7: j in I ; ::_thesis: K . j in A . j
now__::_thesis:_(_(_j_=_i_&_K_._j_in_A_._j_)_or_(_j_<>_i_&_K_._j_in_A_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K . j in A . j
hence  K . j in A . j by A4, A6; ::_thesis: verum
end;
case j <> i ; ::_thesis: K . j in A . j
then  not j in dom (i .--> X9) by A5, TARSKI:def_1;
then  K . j = M . j by FUNCT_4:11;
hence  K . j in A . j by A3, A7, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  K . j in A . j ; ::_thesis: verum
end;
then  K /\ B = [[0]] I by A1;
then  (K . i) /\ (B . i) = ([[0]] I) . i by A2, PBOOLE:def_5;
then  X9 /\ (B . i) = {} by A6, PBOOLE:5;
hence  X9 misses B . i by XBOOLE_0:def_7; ::_thesis: verum
end;
then  union (A . i) misses B . i by ZFMISC_1:80;
then  (union (A . i)) /\ (B . i) = {} by XBOOLE_0:def_7;
then  ((union A) . i) /\ (B . i) = {} by A2, Def2;
then  ((union A) /\ B) . i = {} by A2, PBOOLE:def_5;
hence  ((union A) /\ B) . i = ([[0]] I) . i by PBOOLE:5; ::_thesis: verum
end;
hence  (union A) /\ B = [[0]] I by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:34
for I being set
for A, B being ManySortedSet of I st A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [[0]] I ) holds
union (A /\ B) = (union A) /\ (union B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [[0]] I ) holds
union (A /\ B) = (union A) /\ (union B)
let A, B be ManySortedSet of I; ::_thesis: ( A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [[0]] I ) implies union (A /\ B) = (union A) /\ (union B) )
assume A1: A \/ B is V2() ; ::_thesis: ( ex X, Y being ManySortedSet of I st
( X <> Y & X in A \/ B & Y in A \/ B & not X /\ Y = [[0]] I ) or union (A /\ B) = (union A) /\ (union B) )
assume A2: for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [[0]] I ; ::_thesis: union (A /\ B) = (union A) /\ (union B)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(A_/\_B))_._i_=_((union_A)_/\_(union_B))_._i
let i be set ; ::_thesis: ( i in I implies (union (A /\ B)) . i = ((union A) /\ (union B)) . i )
assume A3: i in I ; ::_thesis: (union (A /\ B)) . i = ((union A) /\ (union B)) . i
 for X9, Y9 being set st X9 <> Y9 & X9 in (A . i) \/ (B . i) & Y9 in (A . i) \/ (B . i) holds
X9 misses Y9
proof
consider M being ManySortedSet of I such that
A4: M in A \/ B by A1, PBOOLE:134;
A5: i in {i} by TARSKI:def_1;
let X9, Y9 be set ; ::_thesis: ( X9 <> Y9 & X9 in (A . i) \/ (B . i) & Y9 in (A . i) \/ (B . i) implies X9 misses Y9 )
assume that
A6: X9 <> Y9 and
A7: X9 in (A . i) \/ (B . i) and
A8: Y9 in (A . i) \/ (B . i) ; ::_thesis: X9 misses Y9
 ( dom (M +* (i .--> X9)) = I & dom (M +* (i .--> Y9)) = I ) by A3, Lm1;
then reconsider Kx = M +* (i .--> X9), Ky = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A9: dom (i .--> Y9) = {i} by FUNCOP_1:13;
then A10: Ky . i = (i .--> Y9) . i by A5, FUNCT_4:13
.= Y9 by FUNCOP_1:72 ;
A11: Ky in A \/ B
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or Ky . j in (A \/ B) . j )
assume A12: j in I ; ::_thesis: Ky . j in (A \/ B) . j
now__::_thesis:_Ky_._j_in_(A_\/_B)_._j
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: Ky . j in (A \/ B) . j
hence  Ky . j in (A \/ B) . j by A8, A10, A12, PBOOLE:def_4; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: Ky . j in (A \/ B) . j
then  not j in dom (i .--> Y9) by A9, TARSKI:def_1;
then  Ky . j = M . j by FUNCT_4:11;
hence  Ky . j in (A \/ B) . j by A4, A12, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  Ky . j in (A \/ B) . j ; ::_thesis: verum
end;
A13: dom (i .--> X9) = {i} by FUNCOP_1:13;
then A14: Kx . i = (i .--> X9) . i by A5, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
 Kx in A \/ B
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or Kx . j in (A \/ B) . j )
assume A15: j in I ; ::_thesis: Kx . j in (A \/ B) . j
now__::_thesis:_(_(_j_=_i_&_Kx_._j_in_(A_\/_B)_._j_)_or_(_j_<>_i_&_Kx_._j_in_(A_\/_B)_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: Kx . j in (A \/ B) . j
hence  Kx . j in (A \/ B) . j by A7, A14, A15, PBOOLE:def_4; ::_thesis: verum
end;
case j <> i ; ::_thesis: Kx . j in (A \/ B) . j
then  not j in dom (i .--> X9) by A13, TARSKI:def_1;
then  Kx . j = M . j by FUNCT_4:11;
hence  Kx . j in (A \/ B) . j by A4, A15, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  Kx . j in (A \/ B) . j ; ::_thesis: verum
end;
then  Kx /\ Ky = [[0]] I by A2, A6, A14, A10, A11;
then  (Kx /\ Ky) . i = {} by PBOOLE:5;
then  X9 /\ Y9 = {} by A3, A14, A10, PBOOLE:def_5;
hence  X9 misses Y9 by XBOOLE_0:def_7; ::_thesis: verum
end;
then  union ((A . i) /\ (B . i)) = (union (A . i)) /\ (union (B . i)) by ZFMISC_1:83;
then  union ((A . i) /\ (B . i)) = ((union A) . i) /\ (union (B . i)) by A3, Def2;
then  union ((A . i) /\ (B . i)) = ((union A) . i) /\ ((union B) . i) by A3, Def2;
then  union ((A . i) /\ (B . i)) = ((union A) /\ (union B)) . i by A3, PBOOLE:def_5;
hence  (union (A /\ B)) . i = ((union A) /\ (union B)) . i by A3, Lm7; ::_thesis: verum
end;
hence  union (A /\ B) = (union A) /\ (union B) by PBOOLE:3; ::_thesis: verum
end;

theorem :: MBOOLEAN:35
for I being set
for A, X being ManySortedSet of I
for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) holds
X c= union A
proof
let I be set ; ::_thesis: for A, X being ManySortedSet of I
for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) holds
X c= union A
let A, X be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) holds
X c= union A
let B be V2() ManySortedSet of I; ::_thesis: ( X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) implies X c= union A )
assume that
A1: X c= union (A \/ B) and
A2: for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ; ::_thesis: X c= union A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (union A) . i )
assume A3: i in I ; ::_thesis: X . i c= (union A) . i
A4: for Y9 being set st Y9 in B . i holds
Y9 misses X . i
proof
consider M being ManySortedSet of I such that
A5: M in B by PBOOLE:134;
let Y9 be set ; ::_thesis: ( Y9 in B . i implies Y9 misses X . i )
assume A6: Y9 in B . i ; ::_thesis: Y9 misses X . i
 dom (M +* (i .--> Y9)) = I by A3, Lm1;
then reconsider K = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A7: dom (i .--> Y9) = {i} by FUNCOP_1:13;
 i in {i} by TARSKI:def_1;
then A8: K . i = (i .--> Y9) . i by A7, FUNCT_4:13
.= Y9 by FUNCOP_1:72 ;
 K in B
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in B . j )
assume A9: j in I ; ::_thesis: K . j in B . j
now__::_thesis:_(_(_j_=_i_&_K_._j_in_B_._j_)_or_(_j_<>_i_&_K_._j_in_B_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K . j in B . j
hence  K . j in B . j by A6, A8; ::_thesis: verum
end;
case j <> i ; ::_thesis: K . j in B . j
then  not j in dom (i .--> Y9) by A7, TARSKI:def_1;
then  K . j = M . j by FUNCT_4:11;
hence  K . j in B . j by A5, A9, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  K . j in B . j ; ::_thesis: verum
end;
then  K /\ X = [[0]] I by A2;
then  (K /\ X) . i = {} by PBOOLE:5;
then  Y9 /\ (X . i) = {} by A3, A8, PBOOLE:def_5;
hence  Y9 misses X . i by XBOOLE_0:def_7; ::_thesis: verum
end;
 X . i c= (union (A \/ B)) . i by A1, A3, PBOOLE:def_2;
then  X . i c= union ((A . i) \/ (B . i)) by A3, Lm6;
then  X . i c= union (A . i) by A4, SETFAM_1:42;
hence  X . i c= (union A) . i by A3, Def2; ::_thesis: verum
end;

theorem :: MBOOLEAN:36
for I being set
for A being V2() V26() ManySortedSet of I st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) holds
union A in A
proof
let I be set ; ::_thesis: for A being V2() V26() ManySortedSet of I st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) holds
union A in A
let A be V2() V26() ManySortedSet of I; ::_thesis: ( ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) implies union A in A )
assume A1: for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ; ::_thesis: union A in A
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or (union A) . i in A . i )
assume A2: i in I ; ::_thesis: (union A) . i in A . i
then  i in dom A by PARTFUN1:def_2;
then  A . i in rng A by FUNCT_1:3;
then A3: A . i is finite by FINSET_1:def_2;
A4: for X9, Y9 being set st X9 in A . i & Y9 in A . i & not X9 c= Y9 holds
Y9 c= X9
proof
let X9, Y9 be set ; ::_thesis: ( X9 in A . i & Y9 in A . i & not X9 c= Y9 implies Y9 c= X9 )
assume that
A5: X9 in A . i and
A6: Y9 in A . i ; ::_thesis: ( X9 c= Y9 or Y9 c= X9 )
consider M being ManySortedSet of I such that
A7: M in A by PBOOLE:134;
 ( dom (M +* (i .--> Y9)) = I & dom (M +* (i .--> X9)) = I ) by A2, Lm1;
then reconsider K1 = M +* (i .--> X9), K2 = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
assume A8: not X9 c= Y9 ; ::_thesis: Y9 c= X9
A9: i in {i} by TARSKI:def_1;
A10: dom (i .--> Y9) = {i} by FUNCOP_1:13;
then A11: K2 . i = (i .--> Y9) . i by A9, FUNCT_4:13
.= Y9 by FUNCOP_1:72 ;
A12: K2 in A
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K2 . j in A . j )
assume A13: j in I ; ::_thesis: K2 . j in A . j
now__::_thesis:_(_(_j_=_i_&_K2_._j_in_A_._j_)_or_(_j_<>_i_&_K2_._j_in_A_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K2 . j in A . j
hence  K2 . j in A . j by A6, A11; ::_thesis: verum
end;
case j <> i ; ::_thesis: K2 . j in A . j
then  not j in dom (i .--> Y9) by A10, TARSKI:def_1;
then  K2 . j = M . j by FUNCT_4:11;
hence  K2 . j in A . j by A7, A13, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  K2 . j in A . j ; ::_thesis: verum
end;
A14: dom (i .--> X9) = {i} by FUNCOP_1:13;
then A15: K1 . i = (i .--> X9) . i by A9, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
 K1 in A
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K1 . j in A . j )
assume A16: j in I ; ::_thesis: K1 . j in A . j
now__::_thesis:_(_(_j_=_i_&_K1_._j_in_A_._j_)_or_(_j_<>_i_&_K1_._j_in_A_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K1 . j in A . j
hence  K1 . j in A . j by A5, A15; ::_thesis: verum
end;
case j <> i ; ::_thesis: K1 . j in A . j
then  not j in dom (i .--> X9) by A14, TARSKI:def_1;
then  K1 . j = M . j by FUNCT_4:11;
hence  K1 . j in A . j by A7, A16, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence  K1 . j in A . j ; ::_thesis: verum
end;
then  ( K1 c= K2 or K2 c= K1 ) by A1, A12;
hence  Y9 c= X9 by A2, A8, A15, A11, PBOOLE:def_2; ::_thesis: verum
end;
 A . i <> {} by A2, PBOOLE:def_13;
then  union (A . i) in A . i by A3, A4, CARD_2:62;
hence  (union A) . i in A . i by A2, Def2; ::_thesis: verum
end;