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 A1, A2, TARSKI:def 3;
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 A3, TARSKI:def 4;
b is_min_depend PA,PB by A5, Def5;
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 A4, A7, TARSKI:def 4;
a /\ u <> {} by A2, A8, XBOOLE_0:def 4;
then A10: not a misses u by XBOOLE_0:def 7;
u in PA by A6, A9;
hence a in B by A1, A9, A10, EQREL_1:def 4; :: thesis: verum
end;
hence ex b being set st
( b in PA '\/' PB & a c= b ) by A5, A7, ZFMISC_1:74; :: thesis: verum
end;
hence PA '<' PA '\/' PB by SETFAM_1:def 2; :: thesis: verum
end;