let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y holds PA '<' PA '\/' PB
thus for PA, PB being a_partition of Y holds PA '<' PA '\/' PB :: thesis: verum
proof
let PA, PB be a_partition of Y; :: thesis: PA '<' PA '\/' PB
for a being set st a in PA holds
ex b being set st
( b in PA '\/' PB & a c= b )
proof
let a be set ; :: thesis: ( a in PA implies ex b being set st
( b in PA '\/' PB & a c= b ) )

assume A1: a in PA ; :: thesis: ex b being set st
( b in PA '\/' PB & a c= b )

then A2: a <> {} by EQREL_1:def 4;
set x = the Element of a;
A3: the Element of a in Y by ;
union (PA '\/' PB) = Y by EQREL_1:def 4;
then consider b being set such that
A4: the Element of a in b and
A5: b in PA '\/' PB by ;
b is_min_depend PA,PB by ;
then b is_a_dependent_set_of PA ;
then consider B being set such that
A6: B c= PA and
B <> {} and
A7: b = union B ;
a in B
proof
consider u being set such that
A8: the Element of a in u and
A9: u in B by ;
a /\ u <> {} by ;
then A10: not a misses u by XBOOLE_0:def 7;
u in PA by A6, A9;
hence a in B by ; :: thesis: verum
end;
hence ex b being set st
( b in PA '\/' PB & a c= b ) by ; :: thesis: verum
end;
hence PA '<' PA '\/' PB by SETFAM_1:def 2; :: thesis: verum
end;