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

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 )

end;for a being set st a in PA holds

ex b being set st

( b in PA '\/' PB & a c= b )

proof

hence
PA '<' PA '\/' PB
by SETFAM_1:def 2; :: thesis: verum
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

( b in PA '\/' PB & a c= b ) by A5, A7, ZFMISC_1:74; :: thesis: verum

end;( 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

hence
ex b being set st
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;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

( b in PA '\/' PB & a c= b ) by A5, A7, ZFMISC_1:74; :: thesis: verum