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 ;
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 ;
b /\ u <> {} by ;
then A11: not b misses u by XBOOLE_0:def 7;
u in PA by ;
hence b in B by ; :: thesis: verum
end;
then A12: b c= a by ;
b is_a_dependent_set_of PA by ;
then a = b by ;
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 ; :: thesis: verum