let Y be non empty set ; 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
verumproof
let PA,
PB be
a_partition of
Y;
PA '<' PA '\/' PB
A1:
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 ;
( a in PA implies ex b being set st
( b in PA '\/' PB & a c= b ) )
assume A2:
a in PA
;
ex b being set st
( b in PA '\/' PB & a c= b )
A3:
a <> {}
by A2, EQREL_1:def 6;
consider x being
Element of
a;
A4:
x in Y
by A2, A3, TARSKI:def 3;
A5:
union (PA '\/' PB) = Y
by EQREL_1:def 6;
consider b being
set such that A6:
x in b
and A7:
b in PA '\/' PB
by A4, A5, TARSKI:def 4;
A8:
b is_min_depend PA,
PB
by A7, Def5;
A9:
b is_a_dependent_set_of PA
by A8, Def2;
consider B being
set such that A10:
B c= PA
and
B <> {}
and A11:
b = union B
by A9, Def1;
A12:
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;
A15:
a /\ u <> {}
by A3, A13, XBOOLE_0:def 4;
A16:
not
a misses u
by A15, XBOOLE_0:def 7;
A17:
u in PA
by A10, A14;
thus
a in B
by A2, A14, A16, A17, EQREL_1:def 6;
verum
end;
thus
ex
b being
set st
(
b in PA '\/' PB &
a c= b )
by A7, A11, A12, ZFMISC_1:92;
verum
end;
thus
PA '<' PA '\/' PB
by A1, SETFAM_1:def 2;
verum
end;