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;
PA '\/' PA '<' PA

proof

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 & ( for d being set st d c= a & d is_a_dependent_set_of PA holds
d = a ) ) by Def2;
then consider B being set such that
A4: ( B c= PA & B <> {} & a = union B ) by Def1;
A5: ( a c= Y & a <> {} ) by A2, EQREL_1:def 6;
consider x being Element of a;
x in a by A5;
then x in Y by A2;
then x in union PA by EQREL_1:def 6;
then consider b being set such that
A6: ( x in b & b in PA ) by TARSKI:def 4;
b in B

proof

consider u being set such that
A7: ( x in u & u in B ) by A4, A5, TARSKI:def 4;
b /\ u <> {} by A6, A7, XBOOLE_0:def 4;
then A8: not b misses u by XBOOLE_0:def 7;
u in PA by A4, A7;
hence b in B by A6, A7, A8, EQREL_1:def 6; :: thesis: verum

end;

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

end;

hence PA '\/' PA '<' PA by SETFAM_1:def 2; :: thesis: verum

end;

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