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 c= Y & a <> {} ) by EQREL_1:def 6;
consider x being Element of a;
A3: x in Y by A2, TARSKI:def 3;
union (PA '\/' PB) = Y by EQREL_1:def 6;
then consider b being set such that
A4: ( x in b & b in PA '\/' PB ) by A3, TARSKI:def 4;
b is_min_depend PA,PB by A4, Def5;
then b is_a_dependent_set_of PA by Def2;
then consider B being set such that
A5: ( B c= PA & B <> {} & b = union B ) by Def1;
a in B

proof

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

end;

hence ex b being set st
( b in PA '\/' PB & a c= b ) by A4, A5, ZFMISC_1:92; :: thesis: verum

end;

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

end;