let Y be non empty set ; :: thesis: for PA being a_partition of Y holds PA '\/' PA = PA

let PA be a_partition of Y; :: thesis: PA '\/' PA = PA

A1: PA '<' PA '\/' PA by Th16;

for a being set st a in PA '\/' PA holds

ex b being set st

( b in PA & a c= b )

hence PA '\/' PA = PA by A1, Th4; :: thesis: verum

let PA be a_partition of Y; :: thesis: PA '\/' PA = PA

A1: PA '<' PA '\/' PA by Th16;

for a being set st a in PA '\/' PA holds

ex b being set st

( b in PA & a c= b )

proof

then
PA '\/' PA '<' PA
by SETFAM_1:def 2;
let a be set ; :: thesis: ( a in PA '\/' PA implies ex b being set st

( b in PA & a c= b ) )

assume A2: a in PA '\/' PA ; :: thesis: ex b being set st

( b in PA & a c= b )

then A3: a is_min_depend PA,PA by Def5;

then a is_a_dependent_set_of PA ;

then consider B being set such that

A4: B c= PA and

B <> {} and

A5: a = union B ;

A6: a <> {} by A2, EQREL_1:def 4;

set x = the Element of a;

the Element of a in a by A6;

then the Element of a in Y by A2;

then the Element of a in union PA by EQREL_1:def 4;

then consider b being set such that

A7: the Element of a in b and

A8: b in PA by TARSKI:def 4;

b in B

b is_a_dependent_set_of PA by A8, Th6;

then a = b by A3, A12;

hence ex b being set st

( b in PA & a c= b ) by A8; :: thesis: verum

end;( b in PA & a c= b ) )

assume A2: a in PA '\/' PA ; :: thesis: ex b being set st

( b in PA & a c= b )

then A3: a is_min_depend PA,PA by Def5;

then a is_a_dependent_set_of PA ;

then consider B being set such that

A4: B c= PA and

B <> {} and

A5: a = union B ;

A6: a <> {} by A2, EQREL_1:def 4;

set x = the Element of a;

the Element of a in a by A6;

then the Element of a in Y by A2;

then the Element of a in union PA by EQREL_1:def 4;

then consider b being set such that

A7: the Element of a in b and

A8: b in PA by TARSKI:def 4;

b in B

proof

then A12:
b c= a
by A5, ZFMISC_1:74;
consider u being set such that

A9: the Element of a in u and

A10: u in B by A5, A6, TARSKI:def 4;

b /\ u <> {} by A7, A9, XBOOLE_0:def 4;

then A11: not b misses u by XBOOLE_0:def 7;

u in PA by A4, A10;

hence b in B by A8, A10, A11, EQREL_1:def 4; :: thesis: verum

end;A9: the Element of a in u and

A10: u in B by A5, A6, TARSKI:def 4;

b /\ u <> {} by A7, A9, XBOOLE_0:def 4;

then A11: not b misses u by XBOOLE_0:def 7;

u in PA by A4, A10;

hence b in B by A8, A10, A11, EQREL_1:def 4; :: thesis: verum

b is_a_dependent_set_of PA by A8, Th6;

then a = b by A3, A12;

hence ex b being set st

( b in PA & a c= b ) by A8; :: thesis: verum

hence PA '\/' PA = PA by A1, Th4; :: thesis: verum