theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b,
c being
Function of
Y,
BOOLEAN for
PA being
a_partition of
Y holds
((Ex (c,PA,G)) '&' (All ((c 'imp' b),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex (
(a '&' b),
PA,
G)