theorem Th46:
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y st
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
CompF (
E,
G)
= ((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J