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 )

proof

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

proof

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;

then A12: b c= a by A5, ZFMISC_1:74;
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;

then PA '\/' PA '<' PA by SETFAM_1:def 2;
hence PA '\/' PA = PA by A1, Th4; :: thesis: verum