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 Th19;
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 A3: a in PA '\/' PA ; :: thesis: ex b being set st
( b in PA & a c= b )
then A4: a is_min_depend PA,PA by Def5;
then a is_a_dependent_set_of PA by Def2;
then consider B being set such that
A6: B c= PA and
B <> {} and
A7: a = union B by Def1;
A8: a <> {} by A3, EQREL_1:def 6;
consider x being Element of a;
x in a by A8;
then x in Y by A3;
then x in union PA by EQREL_1:def 6;
then consider b being set such that
A12: x in b and
A13: b in PA by TARSKI:def 4;
b in B

proof

consider u being set such that
A15: x in u and
A16: u in B by A7, A8, TARSKI:def 4;
b /\ u <> {} by A12, A15, XBOOLE_0:def 4;
then A18: not b misses u by XBOOLE_0:def 7;
u in PA by A6, A16;
hence b in B by A13, A16, A18, EQREL_1:def 6; :: thesis: verum

end;

then A20: b c= a by A7, ZFMISC_1:92;
b is_a_dependent_set_of PA by A13, Th8;
then a = b by A4, A20, Def2;
hence ex b being set st
( b in PA & a c= b ) by A13; :: thesis: verum

end;

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