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