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

proof

consider u being set such that
A13: x in u and
A14: u in B by A6, A11, TARSKI:def 4;
a /\ u <> {} by A3, A13, XBOOLE_0:def 4;
then A16: not a misses u by XBOOLE_0:def 7;
u in PA by A10, A14;
hence a in B by A2, A14, A16, EQREL_1:def 6; :: thesis: verum

end;

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

end;

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

end;